prod_base_smul

Mathlib.GroupTheory.PushoutI

URI: https://scilib.ai/kg/mathlib#Monoid.PushoutI.NormalWord.prod_base_smul

← MathLib Explorer

English

The product of the empty word is the identity.

Русский

Произведение пустого слова равно единице.

LaTeX

$$(empty).prod = 1$$

Lean4

@[simp]
theorem prod_base_smul (h : H) (w : NormalWord d) : (h • w).prod = base φ h * w.prod := by
  simp only [base_smul_def', prod, map_mul, mul_assoc]

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

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

Разделы

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

Аффилиация

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