finiteType_localizationPreserves — Mathlib

English

HoldsForLocalizationAway: if R is a ring, R localized at r is FP over R for any r.

Русский

HoldsForLocalizationAway: для кольца R локализация по r сохраняет FP над R.

LaTeX

$$$\text{HoldsForLocalizationAway }\operatorname{FiniteType}$$$

Lean4

/-- If `S` is a finite type `R`-algebra, then `S' = M⁻¹S` is a finite type `R' = M⁻¹R`-algebra. -/
theorem finiteType_localizationPreserves : RingHom.LocalizationPreserves @RingHom.FiniteType :=
  finiteType_isStableUnderBaseChange.localizationPreserves

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