OAI/Geometry/HeilbronnTriangle/MainOrbitObstruction.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Problem355.MainOrbitObstruction.columnResidueline 14 - lemma
OAI.Problem355.MainOrbitObstruction.reduction_of_mem_orbitline 17 - def
OAI.Problem355.MainOrbitObstruction.encodedColumnsline 27 - theorem
OAI.Problem355.MainOrbitObstruction.small_det_forces_repeated_labels_of_mem_orbitline 33 - theorem
OAI.Problem355.MainOrbitObstruction.det_abs_gt_of_injective_labelsline 51 - theorem
OAI.Problem355.MainOrbitObstruction.lifted_small_event_eq_zero_of_injective_labelsline 69