Documentation
LeanPool
.
TwoColoringOneRound
.
LowerBound
.
N1000000BCompressionComputeS0Int
Search
return to top
source
Imports
Init
Mathlib.Tactic.Common
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.IntervalCases
Mathlib.Tactic.Linarith
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.NormNum
Mathlib.Tactic.Polyrith
Mathlib.Tactic.Positivity
Mathlib.Tactic.Ring
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock0
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock1
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock2
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock4
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock5
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock6
Mathlib.Tactic.Ring.RingNF
Imported by
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
s0IntGoal_all
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0Int
#
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
s0IntGoal_all
(
r
:
Block
)
(
p
q
:
Fin
3
)
:
S0IntGoal
r
p
q