erase_single

Mathlib.Algebra.SkewMonoidAlgebra.Single

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.erase_single

English

Erasing the index a from the basis element single a b yields zero.

Русский

Стирание индекса a из базисного элемента single a b даёт 0.

LaTeX

$$$ erase\ a\ (single a b) = 0 $$$

Lean4

@[simp]
theorem erase_single : erase a (single a b) = 0 := by simp [erase]

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

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

Разделы

Аффилиация

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