Documentation
LeanPool
.
TwoColoringOneRound
.
LowerBound
.
N1000000BCompressionComputeSiIntBlock0Vars8to11
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.N1000000BCompressionComputeSiIntGoal
Mathlib.Tactic.Ring.RingNF
Imported by
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block0_var8
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block0_var9
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block0_var10
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block0_var11
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0Vars8to11
#
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block0_var8
(
p
q
:
Fin
3
)
:
SiIntGoal
⟨
0
,
⋯
⟩
⟨
8
,
⋯
⟩
p
q
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block0_var9
(
p
q
:
Fin
3
)
:
SiIntGoal
⟨
0
,
⋯
⟩
⟨
9
,
⋯
⟩
p
q
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block0_var10
(
p
q
:
Fin
3
)
:
SiIntGoal
⟨
0
,
⋯
⟩
⟨
10
,
⋯
⟩
p
q
source
theorem
Distributed2Coloring
.
LowerBound
.
N1000000BCompressionCompute
.
siIntGoal_block0_var11
(
p
q
:
Fin
3
)
:
SiIntGoal
⟨
0
,
⋯
⟩
⟨
11
,
⋯
⟩
p
q