eq_liftNC — Mathlib

English

If an additive homomorphism l agrees with liftNC on all singles, then l equals liftNC.

Русский

Если аддитивный гомоморфизм l совпадает с liftNC на всех одиночках, то l = liftNC.

LaTeX

$$$$ \ l = liftNC f g \quad \text{if } \forall a,b, l (single a b) = f b * g a $$$$

Lean4

theorem eq_liftNC {R : Type*} [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) (l : SkewMonoidAlgebra k G →+ R)
    (h : ∀ a b, l (single a b) = f b * g a) : l = liftNC f g := by ext a b; simp_all

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