Theorems · Theorem · linear algebra
LinearIndependent.cardinal_lift_le_rank
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
{ι : Type w} {v : ι → M},
LinearIndependent R v → Cardinal.lift.{v, w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, v} (Module.rank R M)- Defined in
- Mathlib.LinearAlgebra.Dimension.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
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
- Set.rangeproof · cited by 4,705
- Cardinalstatement and proof · cited by 2,598
- Nontrivialstatement and proof · cited by 2,416
- le_transproof · cited by 985
- Cardinal.mkstatement and proof · cited by 942
- Cardinal.liftstatement and proof · cited by 583
- LinearIndependentstatement and proof · cited by 560
- Module.rankstatement · cited by 496
- Equiv.toEmbeddingproof · cited by 254
Cited by16
Results whose statement or proof uses this declaration.
- LinearIndependent.cardinal_le_rankproof · cited by 14
- IsLocalizedModule.lift_rank_eqproof · cited by 7
- rank_eq_zero_iffproof · cited by 3
- LinearIndependent.lt_aleph0_of_finiteproof · cited by 3
- Module.Basis.card_le_card_of_linearIndependentproof · cited by 3
- LinearIndependent.cardinalMk_le_finrankproof · cited by 2
- strongRankCondition_iff_forall_rank_lt_aleph0proof · cited by 1
- FixedPoints.rank_le_cardproof · cited by 1
- aleph0_le_rank_of_isEmpty_oreSetproof · cited by 1
- iSupIndep.subtype_ne_bot_le_rankproof · cited by 1
- LinearIndependent.aleph0_le_rankproof · cited by 1
- cardinalMk_algHom_le_rankproof · cited by 1