English
Let a and b commute in a division monoid G. For every integer n, (a b)^{n} = a^{n} b^{n}. In particular, for natural n this reduces to the usual distributive property of powers, and for negative n it uses inverses.
Русский
Пусть a и b коммутируют в делимом моноиде G. Для каждого целого n выполняется (a b)^{n} = a^{n} b^{n}. В частности, для неотрицательного n это обычное распределение степеней, а для отрицательных — через обратные элементы.
LaTeX
$$$Commute(a,b) \Rightarrow \forall n \in \mathbb{Z},\ (ab)^{n} = a^{n} b^{n}$$$
Lean4
@[to_additive AddCommute.zsmul_add]
protected theorem mul_zpow (h : Commute a b) : ∀ n : ℤ, (a * b) ^ n = a ^ n * b ^ n
| (n : ℕ) => by simp [zpow_natCast, h.mul_pow n]
| .negSucc n => by simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]
