English
Compatibility of the liftNC construction with scalar multiplication: applying liftNC after smul by c distributes as f(c) times liftNC on φ.
Русский
Совместимость конструкции liftNC со скалярным умножением: применение liftNC после умножения на c распадается как f(c) умноженное на liftNC(φ).
LaTeX
$$$$liftNC\big( f, g\big)\big( c\cdot \phi\big) = f(c) \cdot liftNC\big(f,g\big)(\phi).$$$$
Lean4
theorem liftNC_smul [MulOneClass G] {R : Type*} [Semiring R] (f : k →+* R) (g : G →* R) (c : k)
(φ : MonoidAlgebra k G) : liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ :=
by
suffices (liftNC (↑f) g).comp (smulAddHom k (MonoidAlgebra k G) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC (↑f) g)
from DFunLike.congr_fun this φ
ext
simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply, AddMonoidHom.coe_mulLeft, smul_single',
liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
