isUnit_of_invertible

Mathlib.Algebra.Group.Invertible.Basic

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

English

An invertible element in a monoid is a unit.

Русский

Инвертируемый элемент в моноиде является единицей.

LaTeX

$$$ \text{Invertible}(a) \Rightarrow \text{IsUnit}(a)$$$

Lean4

theorem isUnit_of_invertible [Monoid α] (a : α) [Invertible a] : IsUnit a :=
  ⟨unitOfInvertible a, rfl⟩

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

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

Разделы

Аффилиация

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