English
For any a ∈ α and integers m,n, a^(m n) = (a^m)^n.
Русский
Для любого a ∈ α и целых m,n верно: a^(m n) = (a^m)^n.
LaTeX
$$$a^{(m n)} = (a^{m})^{n}$$$
Lean4
@[to_additive mul_zsmul']
theorem zpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
| (m : ℕ), (n : ℕ) => by
rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast]
rfl
| (m : ℕ), .negSucc n => by
rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj, ← zpow_natCast]
| .negSucc m, (n : ℕ) => by
rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow, inv_inj, ←
zpow_natCast]
| .negSucc m, .negSucc n =>
by
rw [zpow_negSucc, zpow_negSucc, Int.negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ← zpow_natCast]
rfl
