Documentation
LeanPool
.
TwoColoringOneRound
.
LowerBound
.
N1000000BCompressionCompute
Search
return to top
source
Imports
Init
Mathlib.Tactic.Common
Mathlib.Tactic.ContinuousFunctionalCalculus
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.N1000000BCompressionComputeBase
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSi
Mathlib.Data.Nat.Totient
Mathlib.Tactic.NormNum.GCD
Mathlib.Tactic.Positivity.Finset
Mathlib.Tactic.Ring.RingNF
Mathlib.Algebra.Order.Field.Basic
Mathlib.Data.Sym.Sym2.Init
Imported by
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionCompute
#