English
Raising mk x to the power n yields mk(x.fst, x.snd^n); i.e. (mk x)^n = mk(x.fst, x. snd^n). The base case uses mk_eq_iff to relate the Frobenius iterations.
Русский
Возведение mk x в степень n даёт mk(x.fst, x.snd^n); тождество следует из mk_eq_iff и последовательной работы Фробениуса.
LaTeX
$$$mk\\,K\\,p\\,x^{n} = mk\\,K\\,p\\big( x.1, x.2^{n} \\big)$$$
Lean4
@[simp]
theorem mk_pow (x : ℕ × K) (n : ℕ) : mk K p x ^ n = mk K p (x.1, x.2 ^ n) := by
induction n with
| zero =>
rw [pow_zero, pow_zero, one_def, mk_eq_iff]
exact ⟨0, by simp_rw [← coe_iterateFrobenius, map_one]⟩
| succ n ih =>
rw [pow_succ, pow_succ, ih, mk_mul_mk, mk_eq_iff]
exact ⟨0, by simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul, ← pow_add, mul_assoc, ← pow_add]⟩
