Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000WedderburnData

LeanPool.TwoColoringOneRound.LowerBound.N1000000WedderburnData #

source
@[reducible, inline]
abbrev Distributed2Coloring.LowerBound.N1000000WedderburnData.Q :
Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations
Instances For
    source
    def Distributed2Coloring.LowerBound.N1000000WedderburnData.blockSizes :
    Array ℕ

    Imported auxiliary declaration for the 2-coloring one-round formalization.

    Equations
    Instances For
      source
      def Distributed2Coloring.LowerBound.N1000000WedderburnData.blockScales :
      Array Q

      Imported auxiliary declaration for the 2-coloring one-round formalization.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Distributed2Coloring.LowerBound.N1000000WedderburnData.moduleBasisDen :
        Array ℕ

        Imported auxiliary declaration for the 2-coloring one-round formalization.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Distributed2Coloring.LowerBound.N1000000WedderburnData.moduleBasisNum :
          Array (Array (Array ℤ))

          Imported auxiliary declaration for the 2-coloring one-round formalization.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For