Square-class independence as ZMod 2-linear independence

The multiquadratic degree theorem TauCeti.Multiquadratic.finrank_adjoin_range takes the square-class independence hypothesis in the elaboration-friendly Finset form: no nonempty subset product ∏_{i ∈ S} d i of the radicands is a square in K. The Galois-theoretic arguments instead want the structural form: the classes of the d i in the square-class group Kˣ ⧸ (Kˣ)² are ZMod 2-linearly independent.

The square-class group, the class of a unit, and the equivalence between linear independence of the classes and the Finset form live in TauCeti.FieldTheory.SquareClassGroup.Basic (TauCeti.linearIndependent_squareClass_iff), field-generically and depending only on Mathlib. This file consumes that equivalence to restate the degree theorem against the structural form.

Main results

• TauCeti.Multiquadratic.finrank_adjoin_range_of_linearIndependent: the degree theorem [K(rootᵢ : i) : K] = 2^|ι| restated against linear independence of the unit classes.

theorem TauCeti.Multiquadratic.finrank_adjoin_range_of_linearIndependent {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] {ι : Type u_3} [Finite ι] {d : ι → Kˣ} {root : ι → L} (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) ↑(d i)) [NeZero 2] (hli : LinearIndependent (ZMod 2) fun (i : ι) => squareClass (d i)) : Module.finrank K ↥(IntermediateField.adjoin K (Set.range root)) = 2 ^ Nat.card ι

The multiquadratic degree theorem, restated via linear independence. If the square classes of the radicands d : ι → Kˣ are ZMod 2-linearly independent, then the field generated over K by their square roots root i has degree 2^|ι|. This is finrank_adjoin_range consuming the structural form of square-class independence.