OAI/Algebra/OddKaplansky/OrbitSelection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OddKaplansky.OrbitSelection.Rep line 15
2. instance OAI.OddKaplansky.OrbitSelection.(instance at line 16) line 16
3. def OAI.OddKaplansky.OrbitSelection.representative line 18
4. lemma OAI.OddKaplansky.OrbitSelection.representative_spec line 19
5. lemma OAI.OddKaplansky.OrbitSelection.cover line 29
6. lemma OAI.OddKaplansky.OrbitSelection.card_good line 36
7. lemma OAI.OddKaplansky.OrbitSelection.orbit_injective line 45