case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ 0 < Module.rank R M
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
⊢ 0 < Module.rank R M
obtain ⟨x, hx⟩ := exists_ne (0 : M)
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ 1 ≤ Module.rank R M
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ 0 < Module.rank R M
suffices 1 ≤ Module.rank R M by exact zero_lt_one.trans_le this
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
this : Nontrivial R := Module.nontrivial R M
⊢ 1 ≤ Module.rank R M
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ 1 ≤ Module.rank R M
letI := Module.nontrivial R M
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
this : Nontrivial R := Module.nontrivial R M
⊢ LinearIndependent R fun y => ↑y
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
this : Nontrivial R := Module.nontrivial R M
⊢ 1 ≤ Module.rank R M
suffices LinearIndependent R fun y : ({x} : Set M) => (y : M) by
  simpa using cardinal_le_rank_of_linearIndependent this
no goals
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
this : Nontrivial R := Module.nontrivial R M
⊢ LinearIndependent R fun y => ↑y
exact linearIndependent_singleton hx
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
this : 1 ≤ Module.rank R M
⊢ 0 < Module.rank R M
exact zero_lt_one.trans_le this
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.235792
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
this✝ : Nontrivial R := Module.nontrivial R M
this : LinearIndependent R fun y => ↑y
⊢ 1 ≤ Module.rank R M
simpa using cardinal_le_rank_of_linearIndependent this