lsingle_apply — Mathlib

English

There is an IsScalarTower instance for AddMonoidAlgebra k G over R with the same commuting properties as MonoidAlgebra, via the Multiplicative G correspondence.

Русский

У AddMonoidAlgebra реализовано свойство IsScalarTower поверх R и G через соответствие Multiplicative G.

LaTeX

$$$$IsScalarTower\ R\ k[G]\ k[G].$$$$

Lean4

@[simp]
theorem lsingle_apply [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) : lsingle (R := R) a b = single a b :=
  rfl

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