localizationPreserves

Mathlib.RingTheory.LocalProperties.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.IsStableUnderBaseChange.localizationPreserves

English

The isLocalization_map result shows how a localization map behaves under base change.

Русский

Результат isLocalization_map показывает поведение локализационной карты при базовом изменении.

LaTeX

$$$\\text{IsStableUnderBaseChange }P \\to \\text{IsLocalization_map }P$$$

Lean4

theorem localizationPreserves : LocalizationPreserves P :=
  by
  introv R hf
  exact hP.isLocalization_map _ _ hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru