mk'_mul — Mathlib

English

mk' preserves multiplication: mk'(x·y) equals mk'(x)·mk'(y) when x,y are integral over R.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mk'_mul (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :
    mk' A (x * y) (hx.mul hy) = mk' A x hx * mk' A y hy :=
  algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_mul]

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