ringHomComp_mul — Mathlib

English

If f is injective, then the map χ ↦ χ.ringHomComp f is injective on MulChar.

Русский

Если f инъективен, то отображение χ ↦ χ.ringHomComp f инъективно на MulChar.

LaTeX

$$$$ \\text{If } f \\\\! : R' \\to R'' \text{ is injective, then } \\text{Injective}(\\lambda χ, χ.ringHomComp f). $$$$

Lean4

theorem ringHomComp_mul (χ φ : MulChar R R') (f : R' →+* R'') :
    (χ * φ).ringHomComp f = χ.ringHomComp f * φ.ringHomComp f :=
  by
  ext1
  simp only [ringHomComp_apply, coeToFun_mul, Pi.mul_apply, map_mul]

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