algEquivOfAlgEquiv_eq

Mathlib.RingTheory.Localization.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalization.algEquivOfAlgEquiv_eq

English

The equality of the map part holds for any x in R under the corresponding localizations.

Русский

Равенство отображения сохраняется для любого x в R в соответствующих локализациях.

LaTeX

$$$\\text{algEquivOfAlgEquiv}(S,Q,h,H) = \\text{map}(h, M, ...)$$$

Lean4

theorem algEquivOfAlgEquiv_eq (x : R) : algEquivOfAlgEquiv S Q h H ((algebraMap R S) x) = algebraMap P Q (h x) := by
  simp

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

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

Разделы

Аффилиация

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