annihilator_iSup — Mathlib

English

For any N ⊆ M and any ideal I, I ≤ Ann(N) iff I·N = 0.

Русский

Для любого подмодуля N ⊆ M и идеала I верно: I ≤ Ann(N) тогда и только тогда, когда I·N = 0.

LaTeX

$$$ I \\le \\operatorname{Ann}_R(N) \\iff I \\cdot N = 0. $$$

Lean4

theorem annihilator_iSup (ι : Sort w) (f : ι → Submodule R M) : annihilator (⨆ i, f i) = ⨅ i, annihilator (f i) :=
  le_antisymm (le_iInf fun _ => annihilator_mono <| le_iSup _ _) fun r H =>
    mem_annihilator.2 fun n hn ↦
      iSup_induction f (motive := (r • · = 0)) hn (fun i ↦ mem_annihilator.1 <| (mem_iInf _).mp H i) (smul_zero _)
        fun m₁ m₂ h₁ h₂ ↦ by simp_rw [smul_add, h₁, h₂, add_zero]

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