invertibleOne

Mathlib.Algebra.Group.Invertible.Defs

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

English

In any Monoid, if 1 is invertible, then 1^{-1} = 1.

Русский

В любом моноиде, если 1 обратим, то 1^{-1} = 1.

LaTeX

$$$\\text{If } 1\\text{ is invertible, then } 1^{-1} = 1.$$$

Lean4

/-- `1` is the inverse of itself -/
def invertibleOne [Monoid α] : Invertible (1 : α) :=
  ⟨1, mul_one _, one_mul _⟩

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

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

Разделы

Аффилиация

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