rcons_eq_smul

Mathlib.GroupTheory.CoprodI

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

English

rcons p equals the smul by the head of p on tail p.tail.

Русский

rcons p равен умножению головы p на хвост p.tail.

LaTeX

$$$$ rcons\\, p = \\mathrm{of}\\, p.head \\cdot p.tail $$$$

Lean4

theorem rcons_eq_smul {i} (p : Pair M i) : rcons p = of p.head • p.tail := by simp [of_smul_def]

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

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

Разделы

Аффилиация

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