of'

Mathlib.Algebra.MonoidAlgebra.Defs

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

English

Repeats: single m (-r) = - single m r for all m ∈ M, r ∈ R.

Русский

Повторение: single m (-r) = - single m r для всех m ∈ M, r ∈ R.

LaTeX

$$$\\mathrm{single}(m,-r) = -\\mathrm{single}(m,r).$$$

Lean4

/-- Embedding of a magma with zero `M`, into its magma algebra, having `M` as source. -/
def of' : M → R[M] := fun m => single m 1

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

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

Разделы

Аффилиация

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