OAI/Geometry/HeilbronnTriangle/OrbitSampling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem355.OrbitSampling.orbitFinset line 11
2. theorem OAI.Problem355.OrbitSampling.mem_orbitFinset line 16
3. theorem OAI.Problem355.OrbitSampling.orbitFinset_nonempty line 21
4. theorem OAI.Problem355.OrbitSampling.card_orbitFinset line 25
5. theorem OAI.Problem355.OrbitSampling.uniform_pushforward line 30
6. abbrev OAI.Problem355.OrbitSampling.MainGroup line 53
7. theorem OAI.Problem355.OrbitSampling.sl_averaged_columns_eq_liftedMass line 55
8. theorem OAI.Problem355.OrbitSampling.sl_action_transpose line 73
9. theorem OAI.Problem355.OrbitSampling.sl_action_det line 79
10. def OAI.Problem355.OrbitSampling.integralMatrix line 84
11. theorem OAI.Problem355.OrbitSampling.integralMatrix_reduction_of_mem_orbit line 88
12. theorem OAI.Problem355.OrbitSampling.sl_exact_lifting_identity line 99