mem_dualAnnihilator — Mathlib

English

A linear functional φ lies in W.dualAnnihilator iff φ kills every element of W.

Русский

Линейный функционал φ принадлежит W.dualAnnihilator тогда и только тогда, когда он уничтожает каждый элемент W.

LaTeX

$$φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, φ(w) = 0.$$

Lean4

@[simp]
theorem mem_dualAnnihilator (φ : Module.Dual R M) : φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, φ w = 0 :=
  by
  refine LinearMap.mem_ker.trans ?_
  simp_rw [LinearMap.ext_iff, dualRestrict_apply]
  exact ⟨fun h w hw => h ⟨w, hw⟩, fun h w => h w.1 w.2⟩

Похожие утверждения