Documentation
LeanPool
.
TwoColoringOneRound
.
LowerBound
.
N1000000BCompressionComputeS0
Search
return to top
source
Imports
Init
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeBase
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0Int
Mathlib.Tactic.Positivity.Finset
Imported by
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
compBasis_id_matches_S0
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0
#
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
compBasis_id_matches_S0
(
r
:
Block
)
:
compBasis
r
idDirIdx
=
N1000000WedderburnData.blockScales
[
↑
r
]
!
•
N1000000WeakDuality.S0
r