English
Raising a canonical fraction mk' to a natural power yields the canonical fraction with numerator and denominator raised to that power, with updated coprimality information.
Русский
Возведение канонической дроби mk' в натуральную степень даёт дробь с числителем и знаменателем, возведёнными в эту степень, с обновлённой информацией о взаимной простоте.
LaTeX
$$$ mk' n d hd hdn ^ n = mk' (n^n) (d^n) (by ~) $$$
Lean4
@[simp]
theorem mk'_pow (num : ℤ) (den : ℕ) (hd hdn) (n : ℕ) :
mk' num den hd hdn ^ n =
mk' (num ^ n) (den ^ n) (by simp [Nat.pow_eq_zero, hd]) (by rw [Int.natAbs_pow]; exact hdn.pow _ _) :=
rfl
