Documentation

MIPRE.Foundations.LowDegree.BinaryConstants

Fixed-width zero and one for binary polynomial quotients #

source
def MIPRE.LowDegree.BinaryPolynomial.zeroBits (p : Cost.BitStr) :
Cost.BitStr

Zero and one use the width of the supplied lower-coefficient vector.

Equations
Instances For
    source
    def MIPRE.LowDegree.BinaryPolynomial.oneBits :
    Cost.BitStr → Cost.BitStr
    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryPolynomial.length_zeroBits (p : Cost.BitStr) :
      List.length (zeroBits p) = List.length p
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryPolynomial.length_oneBits (p : Cost.BitStr) :
      List.length (oneBits p) = List.length p
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_zeroBits {R : Type u_1} [CommRing R] (z : R) (p : Cost.BitStr) :
      evalBits z (zeroBits p) = 0
      source
      theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_oneBits {R : Type u_1} [CommRing R] (z : R) (p : Cost.BitStr) (hp : p ≠ []) :
      evalBits z (oneBits p) = 1
      source
      noncomputable def MIPRE.LowDegree.BinaryPolynomial.zeroBitsProg :
      Cost.PolyTimeFun Cost.BitStr Cost.BitStr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.LowDegree.BinaryPolynomial.oneBitsProg :
        Cost.PolyTimeFun Cost.BitStr Cost.BitStr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem MIPRE.LowDegree.BinaryPolynomial.zeroBitsProg_apply (p : Cost.BitStr) :
          zeroBitsProg.toFun p = zeroBits p
          source
          @[simp]
          theorem MIPRE.LowDegree.BinaryPolynomial.oneBitsProg_apply (p : Cost.BitStr) :
          oneBitsProg.toFun p = oneBits p