R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
⊢ ∀ (m : M), ↑(Dual.eval R M) m = 0 → m = 0
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
⊢ ker (Dual.eval R M) = ⊥
rw [ker_eq_bot']
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
m : M
hm : ↑(Dual.eval R M) m = 0
⊢ m = 0
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
⊢ ∀ (m : M), ↑(Dual.eval R M) m = 0 → m = 0
intro m hm
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
m : M
hm : ∀ (x : Dual R M), ↑x m = 0
⊢ m = 0
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
m : M
hm : ↑(Dual.eval R M) m = 0
⊢ m = 0
simp_rw [LinearMap.ext_iff, Dual.eval_apply, zero_apply] at hm
no goals
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
m : M
hm : ∀ (x : Dual R M), ↑x m = 0
⊢ m = 0
exact (Basis.forall_coord_eq_zero_iff _).mp fun i => hm (b.coord i)