Theorems · Theorem · linear algebra
le_rank_iff_exists_linearIndependent
∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
[Module.Free K V] {c : Cardinal.{v}}, c ≤ Module.rank K V ↔ ∃ s, Cardinal.mk ↑s = c ∧ LinearIndepOn K id s- Cited by
- 1 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites28
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Modulestatement and proof · cited by 20,661
- Semiringproof · cited by 13,802
- AddCommGroupstatement and proof · cited by 12,871
- AddCommMonoidproof · cited by 12,281
- Ringstatement and proof · cited by 7,463
- Set.Elemstatement and proof · cited by 7,166
- Set.rangeproof · cited by 4,705
- Cardinalstatement and proof · cited by 2,598
- Nontrivialproof · cited by 2,416
- Set.extproof · cited by 2,266
Cited by1
Results whose statement or proof uses this declaration.
- LinearMap.le_rank_iff_exists_linearIndependentproof · cited by 0