isFullyInvariant_iff_isTwoSided — Mathlib

English

In a ring R, an ideal I is fully invariant if and only if it is two-sided.

Русский

В кольце R идеал I полностью инвариантен тогда и только тогда, когда он двусторонний.

LaTeX

$$$$ I^{{\\mathrm{IsFullyInvariant}}} \\;\\Longleftrightarrow\\; I^{\\mathrm{IsTwoSided}}. $$$$

Lean4

theorem isFullyInvariant_iff_isTwoSided {I : Ideal R} : I.IsFullyInvariant ↔ I.IsTwoSided := by
  simpa only [Submodule.IsFullyInvariant,
    ← MulOpposite.opEquiv.trans (RingEquiv.moduleEndSelf R |>.toEquiv) |>.forall_congr_right, SetLike.le_def,
    I.isTwoSided_iff] using forall_comm

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