Documentation
LeanPool
.
ConwaySoifer
.
Simplified
.
Certificates
.
Checked
.
Sint220000230000
Search
return to top
source
Imports
Init
Mathlib.Tactic.FinCases
LeanPool.ConwaySoifer.Simplified.Certificates.Checkpoints.Sint220000230000
LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sint2200002300000
LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sint2200002300001
LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sint2200002300002
LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sint2200002300003
LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sint2200002300004
LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Sint2200002300005
Imported by
ConwaySoifer
.
Simplified
.
Certificates
.
Sint220000230000
.
excluded43_3
ConwaySoifer
.
Simplified
.
Certificates
.
Sint_220000_230000_checked
Sint 220000 230000
#
Kernel-checked forced assignments and closed-interval exclusions.
source
theorem
ConwaySoifer
.
Simplified
.
Certificates
.
Sint220000230000
.
excluded43_3
:
Certificates.ExcludedOn
(
model43
.
B
3
)
9000000000000
(
model43
.
caps
3
)
(
model43
.
ord
3
)
0
1
100
source
theorem
ConwaySoifer
.
Simplified
.
Certificates
.
Sint_220000_230000_checked
:
Data.Sint220000230000
.
Valid