English
The units α^× form a DivInvMonoid; integer powers zpow are defined by a^n for n ≥ 0 and (a^n)^{-1} for negative n (as specified).
Русский
Единицы α^× образуют DivInvMonoid; zpow определяется как a^n для n ≥ 0 и (a^n)^{-1} для отрицательных n (как указано).
LaTeX
$$$\text{DivInvMonoid}(\alpha^{\times})$ with\ z\_pow : Z → α^× \,\text{defined by the usual rules}$$$
Lean4
/-- Units of a monoid form a `DivInvMonoid`. -/
@[to_additive /-- Additive units of an additive monoid form a `SubNegMonoid`. -/
]
instance instDivInvMonoid : DivInvMonoid αˣ
where
zpow := fun n a ↦
match n, a with
| Int.ofNat n, a => a ^ n
| Int.negSucc n, a => (a ^ n.succ)⁻¹
zpow_zero' := fun a ↦ by simp
zpow_succ' := fun n a ↦ by simp [pow_succ]
zpow_neg' := fun n a ↦ by simp
