English
(x*y)^z = x^z · y^z.
Русский
(x·y)^z = x^z · y^z.
LaTeX
$$$ \forall x,y,z \in \mathbb{N}_\infty,\; (x \cdot y)^z = x^z \cdot y^z. $$$
Lean4
theorem mul_epow : (x * y) ^ z = x ^ z * y ^ z := by
induction z
· rcases lt_trichotomy x 1 with x_0 | rfl | x_2
· simp only [lt_one_iff_eq_zero.1 x_0, zero_mul, zero_epow_top]
· simp only [one_mul, one_epow]
· rcases lt_trichotomy y 1 with y_0 | rfl | y_2
· simp only [lt_one_iff_eq_zero.1 y_0, mul_zero, zero_epow_top]
· simp only [mul_one, one_epow, epow_top x_2]
· rw [epow_top x_2, epow_top y_2, WithTop.top_mul_top]
exact epow_top (one_lt_mul x_2.le y_2)
· simp only [epow_natCast, mul_pow x y]
