OAI/Geometry/HeilbronnTriangle/PairingDivisor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem355.PairingDivisor.dotHom line 10
2. theorem OAI.Problem355.PairingDivisor.dotHom_apply line 13
3. theorem OAI.Problem355.PairingDivisor.exists_pairing_divisor line 15
4. theorem OAI.Problem355.PairingDivisor.integer_subgroup_eq_zmultiples_index line 53
5. def OAI.Problem355.PairingDivisor.pairingDivisor line 60
6. theorem OAI.Problem355.PairingDivisor.pairing_image line 63
7. theorem OAI.Problem355.PairingDivisor.pairingDivisor_dvd_pairing line 67
8. theorem OAI.Problem355.PairingDivisor.exists_pairing_eq_divisor line 73
9. theorem OAI.Problem355.PairingDivisor.dvd_pairingDivisor_iff line 80
10. theorem OAI.Problem355.PairingDivisor.pairingDivisor_pos_and_dvd line 92