mkOfMulEqOne — Mathlib

English

In a commutative monoid, if a and b satisfy a·b = 1, then a is a unit with inverse b.

Русский

В коммутативном моноиде если a·b = 1, то a является единицей с обратной величиной b.

LaTeX

$$$ ab = 1 \Rightarrow a \in \alpha^\times \text{ with inverse } b \text{ (i.e. } a\cdot b=1=b\cdot a). $$$

Lean4

/-- For `a, b` in a `CommMonoid` such that `a * b = 1`, makes a unit out of `a`. -/
@[to_additive /-- For `a, b` in an `AddCommMonoid` such that `a + b = 0`, makes an addUnit out of `a`. -/
    ]
def mkOfMulEqOne [CommMonoid α] (a b : α) (hab : a * b = 1) : αˣ :=
  ⟨a, b, hab, (mul_comm b a).trans hab⟩

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