R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : ↑(toDual b) m = 0
⊢ ↑b.repr m = 0
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : ↑(toDual b) m = 0
⊢ m = 0
rw [← mem_bot R, ← b.repr.ker, mem_ker, LinearEquiv.coe_coe]
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : ↑(toDual b) m = 0
⊢ ∀ (a : ι), ↑(↑b.repr m) a = ↑0 a
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : ↑(toDual b) m = 0
⊢ ↑b.repr m = 0
apply Finsupp.ext
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b✝ : Basis ι R M
m : M
a : ↑(toDual b✝) m = 0
b : ι
⊢ ↑(↑b✝.repr m) b = ↑0 b
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : ↑(toDual b) m = 0
⊢ ∀ (a : ι), ↑(↑b.repr m) a = ↑0 a
intro b
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b✝ : Basis ι R M
m : M
a : ↑(toDual b✝) m = 0
b : ι
⊢ ↑0 (↑b✝ b) = ↑0 b
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b✝ : Basis ι R M
m : M
a : ↑(toDual b✝) m = 0
b : ι
⊢ ↑(↑b✝.repr m) b = ↑0 b
rw [← toDual_eq_repr, a]
no goals
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b✝ : Basis ι R M
m : M
a : ↑(toDual b✝) m = 0
b : ι
⊢ ↑0 (↑b✝ b) = ↑0 b
rfl