R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Module.Dual R M
⊢ ↑(dualRestrict W) φ = 0 ↔ ∀ (w : M), w ∈ W → ↑φ w = 0
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Module.Dual R M
⊢ φ ∈ dualAnnihilator W ↔ ∀ (w : M), w ∈ W → ↑φ w = 0
refine' LinearMap.mem_ker.trans _
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Module.Dual R M
⊢ (∀ (x : { x // x ∈ W }), ↑φ ↑x = ↑0 x) ↔ ∀ (w : M), w ∈ W → ↑φ w = 0
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Module.Dual R M
⊢ ↑(dualRestrict W) φ = 0 ↔ ∀ (w : M), w ∈ W → ↑φ w = 0
simp_rw [LinearMap.ext_iff, dualRestrict_apply]
no goals
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Module.Dual R M
⊢ (∀ (x : { x // x ∈ W }), ↑φ ↑x = ↑0 x) ↔ ∀ (w : M), w ∈ W → ↑φ w = 0
exact ⟨fun h w hw => h ⟨w, hw⟩, fun h w => h w.1 w.2⟩