inv_prod

Mathlib.GroupTheory.CoprodI

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

English

If w is a NeWord in a group, then inv(w).prod = (w.prod)^{-1}.

Русский

Если w — NeWord в группе, то inv(w).prod = (w.prod)^{-1}.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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