OAI/NumberTheory/Jacobsthal/Partitions/NestedCoordinates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos970.ErdosCriticalGeometry.MV line 13
2. abbrev OAI.Erdos970.ErdosCriticalGeometry.Nested line 14
3. def OAI.Erdos970.ErdosCriticalGeometry.nestedX line 16
4. def OAI.Erdos970.ErdosCriticalGeometry.nestedY line 20
5. theorem OAI.Erdos970.ErdosCriticalGeometry.nestedX_C line 23
6. theorem OAI.Erdos970.ErdosCriticalGeometry.nestedX_X_zero line 26
7. theorem OAI.Erdos970.ErdosCriticalGeometry.nestedX_X_one line 29
8. theorem OAI.Erdos970.ErdosCriticalGeometry.nestedY_C line 35
9. theorem OAI.Erdos970.ErdosCriticalGeometry.nestedY_X_zero line 38
10. theorem OAI.Erdos970.ErdosCriticalGeometry.nestedY_X_one line 41
11. def OAI.Erdos970.ErdosCriticalGeometry.nestedEvalHom line 44
12. theorem OAI.Erdos970.ErdosCriticalGeometry.nestedEvalHom_C line 47
13. theorem OAI.Erdos970.ErdosCriticalGeometry.nestedEvalHom_X line 50
14. theorem OAI.Erdos970.ErdosCriticalGeometry.eval_nestedY line 53
15. theorem OAI.Erdos970.ErdosCriticalGeometry.eval_nestedX line 63