lsingle — Mathlib

English

Two R-linear maps φ,ψ from SkewMonoidAlgebra M α to N are equal if they agree on all single a b.

Русский

Два R-линейных отображения φ,ψ из SkewMonoidAlgebra M α в N равны, если они совпадают на всех единичных элементах single a b.

LaTeX

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

Lean4

/-- Interpret `single a` as a linear map. -/
def lsingle {α : Type*} (a : α) [Module R M] : M →ₗ[R] (SkewMonoidAlgebra M α)
    where
  __ := singleAddHom a
  map_smul' _ _ := (smul_single _ _ _).symm

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