single_zero

Mathlib.Algebra.MonoidAlgebra.Defs

URI: https://scilib.ai/kg/mathlib#MonoidAlgebra.single_zero

English

The basis element at m with zero coefficient is the zero element: single m 0 = 0.

Русский

Базисный элемент в позиции m с коэффициентом 0 равен нулю: single m 0 = 0.

LaTeX

$$$\\mathrm{single}(m,0) = 0$$$

Lean4

@[to_additive]
theorem single_zero (m : M) : (single m 0 : MonoidAlgebra R M) = 0 := by simp [single]

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

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

Разделы

Аффилиация

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