annihilator_eq — Mathlib

English

If M and M' are isomorphic as R-modules, then their annihilator ideals in R are equal.

Русский

Пусть M и M' изоморфны как модули над R; их аннигиляторы по отношению к R совпадают.

LaTeX

$$$ M \\cong_R M' \\Rightarrow \\operatorname{Ann}_R(M) = \\operatorname{Ann}_R(M'). $$$

Lean4

theorem annihilator_eq (e : M ≃ₗ[R] M') : Module.annihilator R M = Module.annihilator R M' :=
  (e.annihilator_le_of_surjective e.surjective).antisymm (e.annihilator_le_of_injective e.injective)

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