eq_mk'_iff_mul_eq

Mathlib.RingTheory.Localization.Defs

URI: https://scilib.ai/kg/mathlib#IsLocalization.eq_mk'_iff_mul_eq

English

If z·y = x with y ∈ M, then algebraMap R S z = mk' S x y.

Русский

Если z·y = x и y ∈ M, то f(z) = mk'(x,y).

LaTeX

$$mk'(x,y) = z \\,\\Longrightarrow\\, \\varphi(z) = mk'(x,y) \\; (\\text{при } z y = x)$$

Lean4

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

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

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

Разделы

Аффилиация

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