Exact degrees of sums with coprime binary field degrees

theorem MIPRE.LowDegree.BinaryFiniteField.frobenius_comm {R : Type u_1} [CommRing R] [CharP R 2] (a b : ℕ) (x : R) : (iterateFrobenius R 2 a) ((iterateFrobenius R 2 b) x) = (iterateFrobenius R 2 b) ((iterateFrobenius R 2 a) x)

theorem MIPRE.LowDegree.BinaryFiniteField.iterate_add_delta {R : Type u_1} [CommRing R] (F : R →+ R) (x d : R) (hx : F x = x + d) (hd : F d = d) (n : ℕ) : (⇑F)^[n] x = x + n • d

theorem MIPRE.LowDegree.BinaryFiniteField.nsmul_delta_eq_zero {R : Type u_1} [CommRing R] (F : R →+ R) (x : R) (n : ℕ) (hd : F (F x - x) = F x - x) (hx : (⇑F)^[n] x = x) : n • (F x - x) = 0

theorem MIPRE.LowDegree.BinaryFiniteField.frobenius_period_add_of_coprime {R : Type u_1} [CommRing R] [CharP R 2] (x y : R) (a b n : ℕ) (hab : a.Coprime b) (hx : (iterateFrobenius R 2 a) x = x) (hy : (iterateFrobenius R 2 b) y = y) (hs : (iterateFrobenius R 2 n) (x + y) = x + y) : (iterateFrobenius R 2 n) x = x ∧ (iterateFrobenius R 2 n) y = y

A period of a sum is a period of both summands when their given periods are coprime.

theorem MIPRE.LowDegree.BinaryFiniteField.minpoly_natDegree_dvd_iff_frobenius {L : Type u_2} [Field L] [Algebra (ZMod 2) L] (x : L) (hx : IsIntegral (ZMod 2) x) (n : ℕ) : (minpoly (ZMod 2) x).natDegree ∣ n ↔ x ^ 2 ^ n = x

Binary minimal degree divides exactly the Frobenius periods of an integral element.

theorem MIPRE.LowDegree.BinaryFiniteField.minpoly_natDegree_add_of_coprime {L : Type u_2} [Field L] [Algebra (ZMod 2) L] (x y : L) (hx : IsIntegral (ZMod 2) x) (hy : IsIntegral (ZMod 2) y) (hab : (minpoly (ZMod 2) x).natDegree.Coprime (minpoly (ZMod 2) y).natDegree) : (minpoly (ZMod 2) (x + y)).natDegree = (minpoly (ZMod 2) x).natDegree * (minpoly (ZMod 2) y).natDegree

Summing algebraic binary elements of coprime degrees multiplies their exact degrees.