jacobson_idem — Mathlib

English

For any ideal I, applying the Jacobson operation twice yields the same result as applying it once: Jac(Jac(I)) = Jac(I).

Русский

Для любого идеала I применение операции Якобиона дважды даёт тот же результат, что и однократное применение: Jac(Jac(I)) = Jac(I).

LaTeX

$$$\operatorname{jacobson}(\operatorname{jacobson}(I)) = \operatorname{jacobson}(I)$$$

Lean4

@[simp]
theorem jacobson_idem : jacobson (jacobson I) = jacobson I :=
  le_antisymm (sInf_le_sInf fun _ hJ => ⟨sInf_le hJ, hJ.2⟩) le_jacobson

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