The binomial root has the original coefficient as its norm

The power basis of the supplied binomial quotient computes the root norm. Odd degree cancels the sign of the constant coefficient. Norm multiplicativity then transfers the noncube property to the adjoined root.

theorem Algebraic.Cutwidth.Extractor.Internal.norm_root_binomialModulus {F : Type u_1} [Field F] (a : F) (s : ℕ) : (Algebra.norm F) (AdjoinRoot.root (binomialModulus a s)) = a

theorem Algebraic.Cutwidth.Extractor.Internal.root_binomialModulus_noncube {F : Type u_1} [Field F] (a : F) (s : ℕ) (noncube : ∀ (b : F), b ^ 3 ≠ a) (b : AdjoinRoot (binomialModulus a s)) : b ^ 3 ≠ AdjoinRoot.root (binomialModulus a s)

theorem Algebraic.Cutwidth.Extractor.Internal.binomialModulus_root_properties {F : Type u_1} [Field F] (a : F) (s v : ℕ) (noncube : ∀ (b : F), b ^ 3 ≠ a) : (binomialModulus (AdjoinRoot.root (binomialModulus a s)) v).Monic ∧ Irreducible (binomialModulus (AdjoinRoot.root (binomialModulus a s)) v) ∧ (binomialModulus (AdjoinRoot.root (binomialModulus a s)) v).natDegree = 3 ^ v