compAddChar_injective_left — Mathlib

English

The same evaluation rule for the composed additive character: (ψ.compAddMonoidHom f) a = ψ(f a).

Русский

Та же формула вычисления для составленного характера: (ψ.compAddMonoidHom f) a = ψ(f a).

LaTeX

$$$$ (\psi .\!\!\!\!\!\!\!\!\!\!\!\!\! \, f)(a) = \psi(f(a)). $$$$

Lean4

theorem _root_.MonoidHom.compAddChar_injective_left (ψ : AddChar A M) (hψ : Surjective ψ) :
    Injective fun f : M →* N ↦ f.compAddChar ψ := by rintro f g h; rw [DFunLike.ext'_iff] at h ⊢;
  exact hψ.injective_comp_right h

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