no goals
ι : Type u_2
ι' : Type ?u.592022
R : Type u_1
R₂ : Type ?u.592028
K : Type ?u.592031
M : Type u_3
M' : Type ?u.592037
M'' : Type ?u.592040
V : Type u
V' : Type ?u.592045
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c✝ : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : c • x = 0
⊢ c = 0 ∨ x = 0
exact or_iff_not_imp_right.mpr fun hx => by
  rw [← b.total_repr x, ← LinearMap.map_smul] at hcx
  have := linearIndependent_iff.mp b.linearIndependent (c • b.repr x) hcx
  rw [smul_eq_zero] at this
  exact this.resolve_right fun hr => hx (b.repr.map_eq_zero_iff.mp hr)
ι : Type u_2
ι' : Type ?u.592022
R : Type u_1
R₂ : Type ?u.592028
K : Type ?u.592031
M : Type u_3
M' : Type ?u.592037
M'' : Type ?u.592040
V : Type u
V' : Type ?u.592045
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c✝ : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : ↑(Finsupp.total ι M R ↑b) (c • ↑b.repr x) = 0
hx : ¬x = 0
⊢ c = 0
ι : Type u_2
ι' : Type ?u.592022
R : Type u_1
R₂ : Type ?u.592028
K : Type ?u.592031
M : Type u_3
M' : Type ?u.592037
M'' : Type ?u.592040
V : Type u
V' : Type ?u.592045
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c✝ : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : c • x = 0
hx : ¬x = 0
⊢ c = 0
rw [← b.total_repr x, ← LinearMap.map_smul] at hcx
ι : Type u_2
ι' : Type ?u.592022
R : Type u_1
R₂ : Type ?u.592028
K : Type ?u.592031
M : Type u_3
M' : Type ?u.592037
M'' : Type ?u.592040
V : Type u
V' : Type ?u.592045
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c✝ : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : ↑(Finsupp.total ι M R ↑b) (c • ↑b.repr x) = 0
hx : ¬x = 0
this : c • ↑b.repr x = 0
⊢ c = 0
ι : Type u_2
ι' : Type ?u.592022
R : Type u_1
R₂ : Type ?u.592028
K : Type ?u.592031
M : Type u_3
M' : Type ?u.592037
M'' : Type ?u.592040
V : Type u
V' : Type ?u.592045
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c✝ : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : ↑(Finsupp.total ι M R ↑b) (c • ↑b.repr x) = 0
hx : ¬x = 0
⊢ c = 0
have := linearIndependent_iff.mp b.linearIndependent (c • b.repr x) hcx
ι : Type u_2
ι' : Type ?u.592022
R : Type u_1
R₂ : Type ?u.592028
K : Type ?u.592031
M : Type u_3
M' : Type ?u.592037
M'' : Type ?u.592040
V : Type u
V' : Type ?u.592045
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c✝ : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : ↑(Finsupp.total ι M R ↑b) (c • ↑b.repr x) = 0
hx : ¬x = 0
this : c = 0 ∨ ↑b.repr x = 0
⊢ c = 0
ι : Type u_2
ι' : Type ?u.592022
R : Type u_1
R₂ : Type ?u.592028
K : Type ?u.592031
M : Type u_3
M' : Type ?u.592037
M'' : Type ?u.592040
V : Type u
V' : Type ?u.592045
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c✝ : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : ↑(Finsupp.total ι M R ↑b) (c • ↑b.repr x) = 0
hx : ¬x = 0
this : c • ↑b.repr x = 0
⊢ c = 0
rw [smul_eq_zero] at this
no goals
ι : Type u_2
ι' : Type ?u.592022
R : Type u_1
R₂ : Type ?u.592028
K : Type ?u.592031
M : Type u_3
M' : Type ?u.592037
M'' : Type ?u.592040
V : Type u
V' : Type ?u.592045
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ b₁ : Basis ι R M
i : ι
c✝ : R
x✝ : M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : ↑(Finsupp.total ι M R ↑b) (c • ↑b.repr x) = 0
hx : ¬x = 0
this : c = 0 ∨ ↑b.repr x = 0
⊢ c = 0
exact this.resolve_right fun hr => hx (b.repr.map_eq_zero_iff.mp hr)