commute_coe_inv

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#Units.commute_coe_inv

English

For any a ∈ αˣ, the elements a and a⁻¹ commute in α: a · a⁻¹ = a⁻¹ · a.

Русский

Для любого a ∈ αˣ элементы a и a⁻¹ commute в α: a a⁻¹ = a⁻¹ a.

LaTeX

$$$a \cdot a^{-1} = a^{-1} \cdot a = 1$$$

Lean4

@[to_additive]
theorem commute_coe_inv : Commute (a : α) ↑a⁻¹ := by rw [Commute, SemiconjBy, inv_mul, mul_inv]

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

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

Разделы

Аффилиация

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