nonUnitalAlgHom_ext' — Mathlib

English

Two non-unital k-algebra homomorphisms from SkewMonoidAlgebra k G to A are equal if they agree on all single x 1.

Русский

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

LaTeX

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

Lean4

/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem nonUnitalAlgHom_ext' [DistribMulAction k A] {φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A}
    (h : φ₁.toMulHom.comp (of k G).toMulHom = φ₂.toMulHom.comp (of k G).toMulHom) : φ₁ = φ₂ :=
  nonUnitalAlgHom_ext <| DFunLike.congr_fun h

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