mk'_add_eq_iff_add_mul_eq_mul — Mathlib

English

IsLocalization.mk'_add_eq_iff_add_mul_eq_mul: (mk'(x,y) + z1 = z2) is equivalent to (x + z1·y = z2·y) in S.

Русский

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

LaTeX

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

Lean4

theorem mk'_add_eq_iff_add_mul_eq_mul {x} {y : M} {z₁ z₂} :
    mk' S x y + z₁ = z₂ ↔ algebraMap R S x + z₁ * algebraMap R S y = z₂ * algebraMap R S y := by
  rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]

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