Finite-field membership and exact degree in power-of-two extensions

theorem MIPRE.LowDegree.BinaryFiniteField.mem_range_iff_pow_card {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Finite K] [Algebra K L] (x : L) : x ∈ (algebraMap K L).range ↔ x ^ Nat.card K = x

The fixed points of the base field's cardinality power are exactly that field.

theorem MIPRE.LowDegree.BinaryFiniteField.minpoly_natDegree_of_not_mem_range {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Finite K] [Algebra K L] [Algebra (ZMod 2) L] [FiniteDimensional (ZMod 2) L] (t : ℕ) (hK : Nat.card K = 2 ^ 2 ^ t) (hL : Module.finrank (ZMod 2) L = 2 ^ (t + 1)) (x : L) (hx : x ∉ (algebraMap K L).range) : (minpoly (ZMod 2) x).natDegree = 2 ^ (t + 1)

In a binary extension of degree 2^(t+1), every element outside the index-two subfield has the full extension degree.