distribMulActionHom_ext' — Mathlib

English

If for every a we have f ∘ DistribMulActionHom.single a = g ∘ DistribMulActionHom.single a, then f=g.

Русский

Если для каждого a выполняется f ∘ DistribMulActionHom.single a = g ∘ DistribMulActionHom.single a, то f=g.

LaTeX

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

Lean4

/-- See note [partially-applied ext lemmas]. -/
@[ext]
theorem distribMulActionHom_ext' [DistribMulAction R M] [DistribMulAction R N] {α : Type*}
    {f g : SkewMonoidAlgebra M α →+[R] N}
    (h : ∀ a : α, f.comp (DistribMulActionHom.single a) = g.comp (DistribMulActionHom.single a)) : f = g :=
  distribMulActionHom_ext fun a ↦ DistribMulActionHom.congr_fun (h a)

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