inv

Mathlib.Algebra.Group.Commute.Defs

URI: https://scilib.ai/kg/mathlib#Commute.inv

English

Let G be a division monoid and a, b ∈ G commute. Then (ab)^{-1} = a^{-1} b^{-1}.

Русский

Пусть G — делимый моноид и элементы a, b ∈ G коммутируют. Тогда (ab)^{-1} = a^{-1} b^{-1}.

LaTeX

$$$Commute(a,b) \Rightarrow (ab)^{-1} = a^{-1} b^{-1}$$$

Lean4

@[to_additive]
protected theorem inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by rw [hab.eq, mul_inv_rev]

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

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

Разделы

Аффилиация

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