instIsScalarTowerAtPrimeFractionRing

English

If R and S are Dedekind domains and S is finite over R with a non-zero prime P, then the localization of S at prime complements yields a principal ideal ring.

Русский

Если R и S — Дедекинд domain, S конечен над R и у идеала P не нулевой, то локализация по primeCompl дает кольцо с главными идеалами.

LaTeX

$$$\text{IsPrincipalIdealRing} \; (Localization \; (Algebra.algebraMapSubmonoid S P.primeCompl))$$$

Lean4

instance : IsScalarTower Rₚ K L :=
  of_algebraMap_eq' (ringHom_ext P.primeCompl (RingHom.ext fun x ↦ by simp [RingHom.algebraMap_toAlgebra]))

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