English
In characteristic p with K reduced, two elements mk(x) and mk(y) are equal iff Frobenius iterates satisfy a corresponding identity between the second components after applying suitable iterates.
Русский
При характеристике p и редуцируемом K равенство двух элементов mk(x) и mk(y) эквивалентно равенству после применения итераций Фробениуса к компонентам x,y.
LaTeX
$$$\forall x,y\in\mathbb{N}\times K:\; mk(K,p)x=mk(K,p)y\iff (\mathrm{frobenius}(K,p))^{[y_1]}x_2=(\mathrm{frobenius}(K,p))^{[x_1]}y_2.$$$
Lean4
theorem eq_iff [CommRing K] [IsReduced K] (p : ℕ) [Fact p.Prime] [CharP K p] (x y : ℕ × K) :
mk K p x = mk K p y ↔ (frobenius K p)^[y.1] x.2 = (frobenius K p)^[x.1] y.2 :=
(mk_eq_iff K p x y).trans
⟨fun ⟨z, H⟩ => (frobenius_inj K p).iterate z <| by simpa only [add_comm, iterate_add] using H, fun H => ⟨0, H⟩⟩
