mem_annihilator' — Mathlib

English

A variant of the membership criterion for annihilators involving a linear map built from r and the identity.

Русский

Вариант критерия принадлежности для аннигиляторов с линейным отображением, построенным из r и тождества.

LaTeX

$$$ r \\in N.annihilator' \\iff N \\le \\mathrm{comap}_{(r \\cdot \\mathrm{Id})} \\mathrm{bot}. $$$

Lean4

theorem mem_annihilator' {r} : r ∈ N.annihilator ↔ N ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) ⊥ :=
  mem_annihilator.trans ⟨fun H n hn => (mem_bot R).2 <| H n hn, fun H _ hn => (mem_bot R).1 <| H hn⟩

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