inv_one

Mathlib.Algebra.Group.Defs

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

English

The inverse of the multiplicative identity is itself.

Русский

Обратное единице умножения равно самой единице.

LaTeX

$$$1^{-1} = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_one : (1 : G)⁻¹ = 1 :=
  InvOneClass.inv_one

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

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

Разделы

Аффилиация

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