Frobenius periodicity

If an element of a field of characteristic two is fixed by pi^k and by pi^n, where pi is the Frobenius x -> x^2 and gcd (k, n) = 1, then it is fixed by pi, hence lies in the prime field F_2.

No algebraic closedness is needed: x^2 = x already forces x = 0 or x = 1 in any field.

theorem KasamiCyclicAdditive.FermatCubic.eq_zero_or_one_of_frobenius_fixed {K : Type u_1} [Field K] {x : K} {k n : ℕ} (hkn : k.gcd n = 1) (hk : x ^ 2 ^ k = x) (hn : x ^ 2 ^ n = x) : x = 0 ∨ x = 1

An element fixed by pi^k and pi^n with gcd (k, n) = 1 lies in F_2, i.e. equals 0 or 1.