iInf_pow_eq_bot_of_isDomain — Mathlib

English

For a Noetherian domain R and a proper ideal I ≠ ⊤, the intersection of all powers I^i equals ⊥.

Русский

Для Noetherian_domain R и подходящего идеала I ≠ ⊤ пересечение всех степеней I^i даёт ⊥.

LaTeX

$$$[\\text{IsNoetherianRing } R] \\land [\\text{IsDomain } R] \\land (I \\neq \\top) \\Rightarrow \\bigcap_{i\\in\\mathbb{N}} I^i = \\bot.$$$

Lean4

/-- **Krull's intersection theorem** for Noetherian domains. -/
theorem iInf_pow_eq_bot_of_isDomain [IsNoetherianRing R] [IsDomain R] (h : I ≠ ⊤) : ⨅ i : ℕ, I ^ i = ⊥ :=
  by
  convert I.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors (M := R) h
  simp

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