mk'_add — Mathlib

English

mk' preserves addition: mk'(x+y) equals mk'(x) plus mk'(y) when x,y are integral over R.

Русский

mk' сохраняет сложение: mk'(x+y) = mk'(x) + mk'(y) для интегральных элементов x,y.

LaTeX

$$$\mathrm{mk'}\ A\ (x+y)\ (hx+hy) = \mathrm{mk'}\ A\ x\ hx + \mathrm{mk'}\ A\ y\ hy$$$

Lean4

@[simp]
theorem mk'_add (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :
    mk' A (x + y) (hx.add hy) = mk' A x hx + mk' A y hy :=
  algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_add]

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