lhom_ext — Mathlib

English

An extensionality principle for linear maps from SkewMonoidAlgebra: equality on single a b implies equality of the maps.

Русский

Принцип экстенсиональности для линейных отображений из SkewMonoidAlgebra: равенство на single a b влечет равенство отображений.

LaTeX

$$$\forall a,\ φ( single a b) = ψ( single a b)\; \Rightarrow φ = ψ$$$

Lean4

/-- Two `R`-linear maps from `SkewMonoidAlgebra M α` which agree on each `single x y`
  agree everywhere. -/
theorem lhom_ext {α : Type*} [Module R M] [Module R N] ⦃φ ψ : SkewMonoidAlgebra M α →ₗ[R] N⦄
    (h : ∀ a b, φ (single a b) = ψ (single a b)) : φ = ψ :=
  LinearMap.toAddMonoidHom_injective <| addHom_ext h

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