algHom_ext — Mathlib

English

An ext lemma for DistribMulActionHom with single a, used in partially-applied ext arguments.

Русский

Лемма экстентирования для DistribMulActionHom с единственным a, используемая в частично применяемых аргументах экст.

LaTeX

$$$\forall f,g, (\forall a, f( single a) = g(single a)) \Rightarrow f=g$$$

Lean4

/-- A `k`-algebra homomorphism from `SkewMonoidAlgebra k G` is uniquely defined by its
values on the functions `single a 1`. -/
theorem algHom_ext ⦃φ₁ φ₂ : AlgHom k (SkewMonoidAlgebra k G) A⦄ (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) :
    φ₁ = φ₂ :=
  AlgHom.toLinearMap_injective (lhom_ext' fun a ↦ (LinearMap.ext_ring (h a)))

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