English
If x has finite order, then x is a unit, with inverse x^{ord(x) - 1}.
Русский
Если порядок x конечен, то x является единицей, обратной к x^{ord(x)-1}.
LaTeX
$$$ \forall {M} [Monoid M] {x : M} (hx : IsOfFinOrder x), IsUnit x$$$
Lean4
/-- If the order of `x` is finite, then `x` is a unit with inverse `x ^ (orderOf x - 1)`. -/
@[to_additive (attr := simps) /-- If the additive order of `x` is finite, then `x` is an additive
unit with inverse `(addOrderOf x - 1) • x`. -/
]
noncomputable def unit {M} [Monoid M] {x : M} (hx : IsOfFinOrder x) : Mˣ :=
⟨x, x ^ (orderOf x - 1), by
rw [← _root_.pow_succ', tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one], by
rw [← _root_.pow_succ, tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]⟩
