OAI/Combinatorics/Crossing/TangentTrackIdentity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Zarankiewicz.det2_rotateQuarter_self line 9
2. theorem OAI.Zarankiewicz.normalShift_eq_circleTrackScale line 13
3. theorem OAI.Zarankiewicz.similarity_circleTangentOffset line 33
4. theorem OAI.Zarankiewicz.tangentOffset_eq_normalShift line 38
5. theorem OAI.Zarankiewicz.similarityPoint_squaredLength line 47
6. theorem OAI.Zarankiewicz.physical_circleConnector_strictly_outside line 52