Theorems · Theorem · linear algebra

Module.Basis.card_le_card_of_linearIndependent

∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} [inst_4 : Fintype ι] (b : Module.Basis ι R M) {ι' : Type u_3} [inst_5 : Fintype ι'] {v : ι' → M},
  LinearIndependent R v → Fintype.card ι' ≤ Fintype.card ι

Defined in: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Cited by: 3 results in Mathlib
Foundations: Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring AddCommMonoid Module StrongRankCondition Fintype Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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
Fintypestatement and proof · cited by 7,736
Module.Basisstatement and proof · cited by 1,477
Fintype.cardstatement and proof · cited by 1,386
Cardinal.liftproof · cited by 583
LinearIndependentstatement and proof · cited by 560
StrongRankConditionstatement and proof · cited by 286
Cardinal.mk_fintypeproof · cited by 81
Cardinal.lift_natCastproof · cited by 39
LinearIndependent.cardinal_lift_le_rankproof · cited by 16

Cited by3

Results whose statement or proof uses this declaration.

Ideal.rank_eqproof · cited by 1
Module.Basis.card_le_card_of_leproof · cited by 0
Module.Basis.card_le_card_of_submoduleproof · cited by 0