English
Frobenius on a canonical element mk(x) acts by raising the second coordinate to the p-th power, keeping the first coordinate fixed: frobenius.mk(x) = mk(x.fst, x.snd^p).
Русский
Фробениус на канонический элемент mk(x) действует: первый координат фиксируется, второй возводится в p-ту степень: frobenius.mk(x) = mk(x.fst, x. snd^p).
LaTeX
$$$\\forall x:\\mathbb{N}\\times K,\\; \\mathrm{frobenius}(\\mathrm{PerfectClosure}\\,K\\,p)\\,p\\; (\\mathrm{mk}\\,K\\,p\\,x) = \\mathrm{mk}\\,K\\,p\\big(x.1, x.2^{p}\\big)$$$
Lean4
theorem frobenius_mk (x : ℕ × K) :
(frobenius (PerfectClosure K p) p : PerfectClosure K p → PerfectClosure K p) (mk K p x) = mk _ _ (x.1, x.2 ^ p) :=
by
simp only [frobenius_def]
exact mk_pow K p x p
