mk'_spec_mk

Mathlib.RingTheory.Localization.Defs

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

English

mk'(x,y) + z1 = z2 in S iff x + z1·y = z2·y in R.

Русский

mk'(x,y) + z1 = z2 в S эквивалентно x + z1·y = z2·y в R.

LaTeX

$$mk'(x,y) + z1 = z2 \\iff \\varphi(x) + z1\\varphi(y) = z2\\varphi(y), \\quad \\varphi = \\text{algebraMap } R S$$

Lean4

@[simp]
theorem mk'_spec_mk (x) (y : R) (hy : y ∈ M) : mk' S x ⟨y, hy⟩ * algebraMap R S y = algebraMap R S x :=
  mk'_spec S x ⟨y, hy⟩

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

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

Разделы

Аффилиация

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