algHom_ext — Mathlib

English

For all x in tsze R M, lift f g hg hfg hgf x = f(x.fst) + g(x.snd).

Русский

Для всех x из tsze R M выполняется lift f g hg hfg hgf x = f(x.fst) + g(x.snd).

LaTeX

$$$ lift(f,g,hg,hfg,hgf)(x) = f(x.fst) + g(x.snd) $$$

Lean4

theorem algHom_ext {A} [Semiring A] [Algebra R' A] ⦃f g : tsze R' M →ₐ[R'] A⦄ (h : ∀ m, f (inr m) = g (inr m)) :
    f = g :=
  AlgHom.toLinearMap_injective <| linearMap_ext (fun _r => (f.commutes _).trans (g.commutes _).symm) h

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