Squarefree binary quotients have bijective squaring

theorem MIPRE.LowDegree.BinaryQuotient.square_injective (f : Polynomial (ZMod 2)) (hs : Squarefree f) : Function.Injective fun (x : AdjoinRoot f) => x * x

Squarefree divisibility rules out nilpotents in the binary quotient.

theorem MIPRE.LowDegree.BinaryQuotient.square_bijective (f : Polynomial (ZMod 2)) (hf : f.Monic) (hs : Squarefree f) : Function.Bijective fun (x : AdjoinRoot f) => x * x

A monic quotient is finite in its specified power-basis coordinates, so injective squaring is bijective. No field or irreducibility assumption is used.