Theorems · Theorem · linear algebra
Module.rank_lt_aleph0_iff
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
[StrongRankCondition R], Module.rank R M < Cardinal.aleph0 ↔ Module.Finite R MSee rank_lt_aleph0 for the inverse direction without Module.Free R M.
- Defined in
- Mathlib.LinearAlgebra.Dimension.Free
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Finiteproof · cited by 3,029
- Cardinalstatement and proof · cited by 2,598
- Module.Finitestatement and proof · cited by 1,032
- Module.Freestatement and proof · cited by 597
- Cardinal.aleph0statement and proof · cited by 521
- Module.rankstatement · cited by 496
- StrongRankConditionstatement and proof · cited by 286
- Module.Free.ChooseBasisIndexproof · cited by 133
- Module.Free.chooseBasisproof · cited by 121
Cited by8
Results whose statement or proof uses this declaration.
- Module.finrank_of_not_finiteproof · cited by 8
- Subalgebra.finrank_sup_le_of_freeproof · cited by 2
- Projectivization.IsCollinear_iff_rankproof · cited by 1
- RatFunc.finrank_ratFunc_ratFuncproof · cited by 1
- Basis.linearEquiv_dual_iff_finiteDimensionalproof · cited by 0
- Module.finrank_bot_le_finrank_of_isScalarTower_of_freeproof · cited by 0
- IntermediateField.finrank_sup_leproof · cited by 0
- Module.finrank_top_le_finrank_of_isScalarTower_of_freeproof · cited by 0