of_le_jacobson — Mathlib

English

If I ≤ Jacobson radical of ⊥ in a Noetherian setting, the I-adic topology on M is Hausdorff.

Русский

Если I меньше или равно Jacobson-множителю нуля, тогда I-адическая топология на M тождественна по Гаусдорфу (Hausdorff).

LaTeX

$$$ I \leq \mathrm{jacobson}\, \bot \Rightarrow \mathrm{IsHausdorff}\ I\ M$$$

Lean4

theorem of_le_jacobson (h : I ≤ Ideal.jacobson ⊥) : IsHausdorff I M :=
  ⟨fun x hx ↦ (Ideal.iInf_pow_smul_eq_bot_of_le_jacobson I h).le (by simpa [SModEq.zero] using hx)⟩

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