lsingle — Mathlib

English

Compatibility of liftNC with scalar multiplication in the variation with RingHom and MonoidHom, mirroring the additive case.

Русский

Совместимость liftNC со скалярным умножением в вариации с RingHom и MonoidHom, аналогично случаям сложения.

LaTeX

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

Lean4

/-- A copy of `Finsupp.lsingle` for `AddMonoidAlgebra`. -/
abbrev lsingle [Semiring R] [Semiring k] [Module R k] (a : G) : k →ₗ[R] AddMonoidAlgebra k G :=
  Finsupp.lsingle a

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