English
An element r belongs to the annihilator of the span of a set s exactly when r kills every element of s.
Русский
Элемент r принадлежит аннигилятору линейного охвата множества s тогда и только тогда, когда r убивает каждый элемент s.
LaTeX
$$$ r \\in \\operatorname{Ann}_R(\\operatorname{span}_R(s)) \\iff \\forall n \\in s,\\; r \\cdot n = 0. $$$
Lean4
theorem mem_annihilator_span (s : Set M) (r : R) : r ∈ (Submodule.span R s).annihilator ↔ ∀ n : s, r • (n : M) = 0 :=
by
rw [Submodule.mem_annihilator]
constructor
· intro h n
exact h _ (Submodule.subset_span n.prop)
· intro h n hn
refine Submodule.span_induction ?_ ?_ ?_ ?_ hn
· intro x hx
exact h ⟨x, hx⟩
· exact smul_zero _
· intro x y _ _ hx hy
rw [smul_add, hx, hy, zero_add]
· intro a x _ hx
rw [smul_comm, hx, smul_zero]
