injective_ringHomComp — Mathlib

English

If f is injective, then χ ↦ χ.ringHomComp f is injective on MulChar (dup).

Русский

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

LaTeX

$$$$ \\text{Injective}(\\lambda χ, χ.ringHomComp f). $$$$

Lean4

theorem injective_ringHomComp {f : R' →+* R''} (hf : Function.Injective f) :
    Function.Injective (ringHomComp (R := R) · f) := by
  simpa only [Function.Injective, MulChar.ext_iff, ringHomComp, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] using
    fun χ χ' h a ↦ hf (h a)

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