mk'_eq_iff_eq_mul

Mathlib.RingTheory.Localization.Defs

URI: https://scilib.ai/kg/mathlib#IsLocalization.mk'_eq_iff_eq_mul

English

mk' S x1 y1 = mk' S x2 y2 iff f(y2·x1) = f(y1·x2).

Русский

mk'(x1,y1) = mk'(x2,y2) тогда и только тогда, когда f(y2·x1) = f(y1·x2).

LaTeX

$$mk'(x1,y1) = mk'(x2,y2) \\iff f(y2\\cdot x1) = f(y1\\cdot x2)$$

Lean4

theorem mk'_eq_iff_eq_mul {x} {y : M} {z} : mk' S x y = z ↔ algebraMap R S x = z * algebraMap R S y :=
  (toLocalizationMap M S).mk'_eq_iff_eq_mul

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

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

Разделы

Аффилиация

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