mul_invOf_self

Mathlib.Algebra.Group.Invertible.Defs

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

English

For invertible a, a^{-1} exists and behaves as the two-sided inverse with a.

Русский

Для обратимого a существует обратное и оно является двусторонним обратным к a.

LaTeX

$$$\text{Invertible}(a) \implies (a)^{-1} a = a (a)^{-1} = 1$$$

Lean4

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

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

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

Разделы

Аффилиация

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