inv_last

Mathlib.GroupTheory.CoprodI

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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