finitePresentation_localizationPreserves

English

Finite presentation is preserved by localization: localizing the base ring or the target ring preserves finite presentation.

Русский

Локализация базового кольца или целевого кольца сохраняет конечнопредставление.

LaTeX

$$$\text{LocalizationPreserves }\operatorname{FinitePresentation}.$$$

Lean4

/-- Being finitely-presented is preserved by localizations. -/
theorem finitePresentation_localizationPreserves : LocalizationPreserves @FinitePresentation :=
  finitePresentation_isStableUnderBaseChange.localizationPreserves

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