of

Mathlib.Algebra.MonoidAlgebra.Defs

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.of

← MathLib Explorer

English

Same as Neg Apply: (-x) m = - x m for all m ∈ M.

Русский

То же, что и Neg Apply: (-x) m = - x m для всех m ∈ M.

LaTeX

$$$(-x)(m) = -x(m).$$$

Lean4

/-- Embedding of a magma with zero into its magma algebra. -/
def of [AddZeroClass M] : Multiplicative M →* R[M] :=
  { ofMagma R M with
    toFun := fun a => single a 1
    map_one' := rfl }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru