commute_invOf

Mathlib.Algebra.Group.Invertible.Basic

URI: https://scilib.ai/kg/mathlib#commute_invOf

← MathLib Explorer

English

In any monoid, an element m and its inverse m^{-1} commute: m m^{-1} = m^{-1} m.

Русский

В любом моноиде элемент m и его обратное m^{-1} commute: m m^{-1} = m^{-1} m.

LaTeX

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

Lean4

theorem commute_invOf {M : Type*} [One M] [Mul M] (m : M) [Invertible m] : Commute m (⅟m) :=
  calc
    m * ⅟m = 1 := mul_invOf_self m
    _ = ⅟m * m := (invOf_mul_self m).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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