prod_empty

Mathlib.GroupTheory.CoprodI

URI: https://scilib.ai/kg/mathlib#Monoid.CoprodI.Word.prod_empty

English

The product of the empty word equals the identity element 1 in CoprodI M.

Русский

Произведение пустого слова равно тождественному элементу 1 в CoprodI M.

LaTeX

$$$ \\mathrm{prod}(\\mathrm{empty}) = 1$$$

Lean4

@[simp]
theorem prod_empty : prod (empty : Word M) = 1 :=
  rfl

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

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

Разделы

Аффилиация

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