lift_comp

Mathlib.RingTheory.Localization.Away.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalization.Away.lift_comp

English

The composition of Lift with the algebra map equals g: (lift x hg) ∘ algebraMap_R^S = g.

Русский

Смешение Lift с алгебраической картой дает g: (lift x hg) ∘ algebraMap_R^S = g.

LaTeX

$$$(\\operatorname{lift}\\; x\\; hg) \\circ (\\operatorname{algebraMap}_{R,S}) = g$$$

Lean4

@[simp]
theorem lift_comp (hg : IsUnit (g x)) : (lift x hg).comp (algebraMap R S) = g :=
  IsLocalization.lift_comp _

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

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

Разделы

Аффилиация

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