liftNC_smul — Mathlib

English

A variant of liftNC_smul for AddMonoidAlgebra, expressing compatibility with smul by c via RingHom and MonoidHom on Multiplicative G.

Русский

Вариант liftNC_smul для AddMonoidAlgebra: совместимость со скалярным умножением на c через RingHom и MonoidHom на Multiplicative G.

LaTeX

$$$$liftNC\big( (f: k\to+ R) , (g: Multiplicative G \to R) \big)(c\cdot φ) = f(c) \cdot liftNC( f,g)(φ).$$$$

Lean4

theorem liftNC_smul {R : Type*} [AddZeroClass G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (c : k)
    (φ : MonoidAlgebra k G) : liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ :=
  @MonoidAlgebra.liftNC_smul k (Multiplicative G) _ _ _ _ f g c φ

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