annihilator_isRadical — Mathlib

English

The annihilator of a semisimple module over a commutative ring is a radical ideal.

Русский

Аннигилятор полупрямого модуля над коммутативным кольцом является радикальным идеалом.

LaTeX

$$(Module.annihilator R M).IsRadical$$

Lean4

/-- The annihilator of a semisimple module over a commutative ring is a radical ideal. -/
theorem annihilator_isRadical (R) [CommRing R] [Module R M] [IsSemisimpleModule R M] :
    (Module.annihilator R M).IsRadical :=
  by
  rw [← Submodule.annihilator_top, ← sSup_simples_eq_top, sSup_eq_iSup', Submodule.annihilator_iSup]
  exact Ideal.isRadical_iInf _ fun i ↦ (i.2.annihilator_isMaximal).isPrime.isRadical

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