R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
⊢ dualAnnihilator ⊤ ≤ ⊥
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
⊢ dualAnnihilator ⊤ = ⊥
rw [eq_bot_iff]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
v : Module.Dual R M
⊢ v ∈ dualAnnihilator ⊤ → v ∈ ⊥
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
⊢ dualAnnihilator ⊤ ≤ ⊥
intro v
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
v : Module.Dual R M
⊢ (∀ (w : M), ↑v w = 0) → v = 0
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
v : Module.Dual R M
⊢ v ∈ dualAnnihilator ⊤ → v ∈ ⊥
simp_rw [mem_dualAnnihilator, mem_bot, mem_top, forall_true_left]
no goals
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
v : Module.Dual R M
⊢ (∀ (w : M), ↑v w = 0) → v = 0
exact fun h => LinearMap.ext h