mk'_eq_iff_eq

Mathlib.RingTheory.Localization.Defs

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

← MathLib Explorer

English

mk' S x y = z iff algebraMap R S x = z · algebraMap R S y.

Русский

mk'(x,y) = z тогда и только тогда, когда f(x) = z·f(y).

LaTeX

$$mk'(x,y) = z \\iff f(x) = z \\cdot f(y), \\quad f = algebraMap R S$$

Lean4

theorem mk'_eq_iff_eq {x₁ x₂} {y₁ y₂ : M} :
    mk' S x₁ y₁ = mk' S x₂ y₂ ↔ algebraMap R S (y₂ * x₁) = algebraMap R S (y₁ * x₂) :=
  (toLocalizationMap M S).mk'_eq_iff_eq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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