finite_factors — Mathlib

English

Localization at a prime ideal yields a Dedekind domain.

Русский

Локализация по прайму приводит к Дедекендовому домену.

LaTeX

$$$\forall P [P.IsPrime], IsDedekindDomain (Localization.AtPrime P)$$$

Lean4

/-- Only finitely many maximal ideals of `R` divide a given nonzero ideal. -/
theorem finite_factors {I : Ideal R} (hI : I ≠ 0) : {v : HeightOneSpectrum R | v.asIdeal ∣ I}.Finite :=
  by
  rw [← Set.finite_coe_iff, Set.coe_setOf]
  haveI h_fin := fintypeSubtypeDvd I hI
  refine Finite.of_injective (fun v => (⟨(v : HeightOneSpectrum R).asIdeal, v.2⟩ : { x // x ∣ I })) ?_
  intro v w hvw
  exact Subtype.coe_injective (HeightOneSpectrum.ext (by simpa using hvw))

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