LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntGoal #
@[reducible, inline]
abbrev
Distributed2Coloring.LowerBound.N1000000BCompressionCompute.S0IntGoal
(r : Block)
(p q : Fin 3)
:
Imported auxiliary declaration for the 2-coloring one-round formalization.
Equations
- One or more equations did not get rendered due to their size.