English
Exponentiation on ENat satisfies the law x^(y·z) = (x^y)^z for all x,y,z.
Русский
На ENat выполняется тождество степеней: x^(y·z) = (x^y)^z для любых x,y,z.
LaTeX
$$x^{(y\\cdot z)} = (x^{y})^{z}$$
Lean4
theorem epow_mul : x ^ (y * z) = (x ^ y) ^ z :=
by
rcases eq_or_ne y 0 with y_0 | y_0
· simp [y_0]
rcases eq_or_ne z 0 with z_0 | z_0
· simp [z_0]
rcases lt_trichotomy x 1 with x_0 | rfl | x_2
· rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]
· simp only [one_epow]
· induction y
· rw [top_mul z_0, epow_top x_2, top_epow z_0]
induction z
· rw [mul_top y_0, epow_top x_2]
apply (epow_top _).symm
apply (epow_right_mono (one_le_iff_ne_zero.1 x_2.le) (one_le_iff_ne_zero.2 y_0)).trans_lt'
simp only [x_2, epow_one]
· simp only [← Nat.cast_mul, epow_natCast, pow_mul x]
