Theorems · Theorem · linear algebra

LinearIndependent.fintype_card_le_finrank

∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] {ι : Type u_1} [inst_5 : Fintype ι] {b : ι → M},
  LinearIndependent R b → Fintype.card ι ≤ Module.finrank R M

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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.finrankstatement and proof · cited by 1,770
Fintype.cardstatement · cited by 1,386
Module.Finitestatement and proof · cited by 1,032
LinearIndependentstatement and proof · cited by 560
StrongRankConditionstatement and proof · cited by 286
Cardinal.mk_fintypeproof · cited by 81
LinearIndependent.cardinalMk_le_finrankproof · cited by 2

Cited by4

Results whose statement or proof uses this declaration.

finrank_algHomproof · cited by 3
AddChar.card_addChar_leproof · cited by 1
LinearIndependent.finset_card_le_finrankproof · cited by 1
LinearMap.normDet_sq_eq_det_gramproof · cited by 0