annihilator_quotient — Mathlib

English

In a two-sided setting with a quotient by N, the annihilator of the quotient R ⧸ I under a two-sided ideal I coincides with I.

Русский

В случае двусторонних колебаний: аннигилятор R/I равен I.

LaTeX

$$$\\operatorname{Module.annihilator} R (R/I) = I$$$

Lean4

theorem annihilator_quotient : Module.annihilator R (M ⧸ N) = N.colon ⊤ := by
  simp_rw [SetLike.ext_iff, Module.mem_annihilator, ← annihilator_map_mkQ_eq_colon, mem_annihilator, map_top,
    LinearMap.range_eq_top.mpr (mkQ_surjective N), mem_top, forall_true_left, forall_const]

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