algHom_ext' — Mathlib

English

An algebra-hom ext principle: two algebra homomorphisms from SkewMonoidAlgebra k G to A are equal if they agree on all single x 1.

Русский

Принцип экстенсивности алгебро-гомоморфизмов: два гомоморфизма от SkewMonoidAlgebra k G в A равны, если они совпадают на всем single x 1.

LaTeX

$$$\forall x,\ φ_1(single x 1) = φ_2(single x 1) \Rightarrow φ_1 = φ_2$$$

Lean4

@[ext high]
theorem algHom_ext' ⦃φ₁ φ₂ : AlgHom k (SkewMonoidAlgebra k G) A⦄
    (h : (φ₁ : SkewMonoidAlgebra k G →* A).comp (of k G) = (φ₂ : SkewMonoidAlgebra k G →* A).comp (of k G)) : φ₁ = φ₂ :=
  algHom_ext <| DFunLike.congr_fun h

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