Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Condenser.Modulus.Binary.Internal.Basic

Degree and the base quadratic of the binary modulus family #

The leading exponent is strictly larger than the two remaining exponents. At exponent zero, the quadratic has no root in the two-element field.

source
theorem Algebraic.Cutwidth.Extractor.Internal.binaryModulus_monic (s : ℕ) :
(binaryModulus s).Monic
source
theorem Algebraic.Cutwidth.Extractor.Internal.binaryModulus_natDegree (s : ℕ) :
(binaryModulus s).natDegree = 2 * 3 ^ s
source
theorem Algebraic.Cutwidth.Extractor.Internal.binaryModulus_zero_irreducible :
Irreducible (binaryModulus 0)