inv_head

Mathlib.GroupTheory.CoprodI

URI: https://scilib.ai/kg/mathlib#Monoid.CoprodI.NeWord.inv_head

English

For NeWord w in a group, inv_head: w.inv.head = w.last^{-1}.

Русский

Для NeWord w в группе inv_head: w.inv.head = w.last^{-1}.

LaTeX

$$$$\\text{inv}(w).head = w.last^{-1}.$$$$

Lean4

@[simp]
theorem inv_head {i j} (w : NeWord G i j) : w.inv.head = w.last⁻¹ := by induction w <;> simp [inv, *]

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

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

Разделы

Аффилиация

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