invOf_mul_self

Mathlib.Algebra.Group.Invertible.Defs

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

English

If a is invertible, then a^{-1} * a = 1 and a * a^{-1} = 1.

Русский

Если a обратимо, то a^{-1} a = 1 и a a^{-1} = 1.

LaTeX

$$$a^{-1} a = 1 \quad\text{and}\quad a a^{-1} = 1$$$

Lean4

theorem invOf_mul_self [Mul α] [One α] (a : α) [Invertible a] : ⅟a * a = 1 :=
  invOf_mul_self' _

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

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

Разделы

Аффилиация

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