lhom_ext' — Mathlib

English

Same extensional principle for linear maps; a variant stating ext via lsingle.

Русский

Та же экстенсионная принципиальная формулировка для линейных отображений; вариант через lsingle.

LaTeX

$$$\forall a, φ\circ (lsingle a) = ψ\circ (lsingle a) \Rightarrow φ = ψ$$$

Lean4

@[ext high]
theorem lhom_ext' {α : Type*} [Module R M] [Module R N] ⦃φ ψ : SkewMonoidAlgebra M α →ₗ[R] N⦄
    (h : ∀ a, φ.comp (lsingle a) = ψ.comp (lsingle a)) : φ = ψ :=
  lhom_ext fun a ↦ LinearMap.congr_fun (h a)

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