case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.376396
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
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
⊢ (#κ) ≤ (#ι)

case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.376396
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
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
⊢ (#ι) ≤ (#κ)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.376396
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
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
⊢ (#κ) = (#ι)
apply le_antisymm
no goals
case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.376396
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
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
⊢ (#κ) ≤ (#ι)
exact linearIndependent_le_basis b v i
case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.376396
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
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
this : Nontrivial R
⊢ (#ι) ≤ (#κ)
case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.376396
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
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
⊢ (#ι) ≤ (#κ)
haveI : Nontrivial R := nontrivial_of_invariantBasisNumber R
no goals
case a
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.376396
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
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
m : LinearIndependent.Maximal i
this : Nontrivial R
⊢ (#ι) ≤ (#κ)
exact infinite_basis_le_maximal_linearIndependent b v i m