case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ (#κ) ≤ (#ι)

case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Infinite ι
⊢ (#κ) ≤ (#ι)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
⊢ (#κ) ≤ (#ι)
cases fintypeOrInfinite ι
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ (#κ) ≤ ↑(Fintype.card ι)
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ (#κ) ≤ (#ι)
rw [Cardinal.mk_fintype ι]
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ (#κ) ≤ ↑(Fintype.card ι)
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ (#κ) ≤ ↑(Fintype.card ι)
haveI : Nontrivial R := nontrivial_of_invariantBasisNumber R
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ (#κ) ≤ ↑(Fintype.card ↑(range ↑b))
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ (#κ) ≤ ↑(Fintype.card ι)
rw [Fintype.card_congr (Equiv.ofInjective b b.injective)]
no goals
case inl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ (#κ) ≤ ↑(Fintype.card ↑(range ↑b))
exact linearIndependent_le_span v i (range b) b.span_eq
no goals
case inr
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.369966
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
κ : Type u_1
v : κ → M
i : LinearIndependent R v
val✝ : Infinite ι
⊢ (#κ) ≤ (#ι)
exact linearIndependent_le_infinite_basis b v i