unitOfInvertible — Mathlib

English

There is a canonical way to form a unit from an invertible element in a monoid.

Русский

Существует канонический способ получить единицу из инвертируемого элемента в моноиде.

LaTeX

$$$ \text{unitOfInvertible} : \text{IsInvertible in monoid} \Rightarrow \text{Unit}$$$

Lean4

/-- An `Invertible` element is a unit. -/
@[simps]
def unitOfInvertible [Monoid α] (a : α) [Invertible a] : αˣ
    where
  val := a
  inv := ⅟a
  val_inv := by simp
  inv_val := by simp

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