Theorems · Theorem · linear algebra

finrank_top

∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.finrank R ↥⊤ = Module.finrank R M

Defined in: Mathlib.LinearAlgebra.Dimension.Finrank
Cited by: 31 results in Mathlib
Foundations: Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring AddCommMonoid Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Modulestatement and proof · cited by 20,661
Semiringstatement and proof · cited by 13,802
AddCommMonoidstatement and proof · cited by 12,281
Top.topstatement · cited by 9,680
Submodulestatement · cited by 7,192
Module.finrankstatement · cited by 1,770
Module.rankproof · cited by 496
Cardinal.toNatproof · cited by 153
rank_topproof · cited by 9

Cited by31

Results whose statement or proof uses this declaration.

Field.finSepDegree_eq_finrank_of_isSeparableproof · cited by 7
Submodule.finrank_add_finrank_orthogonalproof · cited by 6
Subalgebra.bot_eq_top_iff_finrank_eq_oneproof · cited by 5
IntermediateField.finrank_top'proof · cited by 4
AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_oneproof · cited by 4
RootPairing.linearIndepOn_root_baseOfproof · cited by 3
Field.primitive_element_iff_minpoly_natDegree_eqproof · cited by 2
Module.Dual.finrank_ker_add_one_of_ne_zeroproof · cited by 2
Module.Dual.isCompl_ker_of_disjoint_of_ne_botproof · cited by 2
Submodule.finrank_add_eq_of_isComplproof · cited by 2
RootPairing.rootSpan_eq_top_iffproof · cited by 1
EuclideanGeometry.exists_circumcenter_eq_of_cosphericalproof · cited by 1