Theorems · Theorem · linear algebra
Module.rank_lt_aleph0
∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R] [Module.Finite R M], Module.rank R M < Cardinal.aleph0
The rank of a finite module is finite.
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- Finsetproof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Top.topproof · cited by 9,680
- SetLike.coeproof · cited by 8,199
- Set.Elemproof · cited by 7,166
- Cardinalstatement · cited by 2,598
- Submodule.spanproof · cited by 1,504
- Module.Finitestatement and proof · cited by 1,032
- LE.le.trans_ltproof · cited by 795
Cited by23
Results whose statement or proof uses this declaration.
- Module.finrank_eq_rankproof · cited by 29
- Submodule.finrank_leproof · cited by 20
- Submodule.finrank_monoproof · cited by 11
- Matrix.rank_mul_le_leftproof · cited by 5
- Module.finrank_eq_zero_iff_of_freeproof · cited by 4
- Module.finrank_prodproof · cited by 4
- Module.finrank_top_le_finrank_of_isScalarTowerproof · cited by 4
- Submodule.finrank_eq_rankproof · cited by 3
- Matrix.rank_mul_le_rightproof · cited by 2
- Subalgebra.finrank_sup_le_of_freeproof · cited by 2
- LinearMap.finrank_le_finrank_of_injectiveproof · cited by 2
- LinearMap.finrank_range_leproof · cited by 2