iInf_pow_eq_bot_of_isLocalRing — Mathlib

English

For a Noetherian local ring R and a proper ideal I ≠ ⊤, the intersection ∩_{i≥0} I^i equals ⊥.

Русский

Для Noetherian локального кольца R и подходящего идеала I ≠ ⊤, пересечение ∩_{i≥0} I^i равно нулю.

LaTeX

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

Lean4

/-- **Krull's intersection theorem** for Noetherian local rings. -/
theorem iInf_pow_eq_bot_of_isLocalRing [IsNoetherianRing R] [IsLocalRing R] (h : I ≠ ⊤) : ⨅ i : ℕ, I ^ i = ⊥ :=
  by
  convert I.iInf_pow_smul_eq_bot_of_isLocalRing (M := R) h
  ext i
  rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one]

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