OAI/Algebra/OddKaplansky/FiniteChoice.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.FiniteChoice.orderedIndex line 14
  2. def OAI.OddKaplansky.FiniteChoice.table line 16
  3. lemma OAI.OddKaplansky.FiniteChoice.table_injective line 18
  4. def OAI.OddKaplansky.FiniteChoice.functionOrder line 24
  5. def OAI.OddKaplansky.FiniteChoice.tupleOrder line 27
  6. def OAI.OddKaplansky.FiniteChoice.residueOrder line 30
  7. def OAI.OddKaplansky.FiniteChoice.multiplicativeOrder line 33
  8. lemma OAI.OddKaplansky.FiniteChoice.exists_primitive line 35
  9. def OAI.OddKaplansky.FiniteChoice.candidates line 41
  10. lemma OAI.OddKaplansky.FiniteChoice.candidates_nonempty line 42
  11. def OAI.OddKaplansky.FiniteChoice.first line 50
  12. lemma OAI.OddKaplansky.FiniteChoice.first_spec line 51
  13. lemma OAI.OddKaplansky.FiniteChoice.first_le line 54
  14. def OAI.OddKaplansky.FiniteChoice.primitive line 57
  15. lemma OAI.OddKaplansky.FiniteChoice.primitive_spec line 58
  16. lemma OAI.OddKaplansky.FiniteChoice.primitive_le line 59