OAI/Algebra/OddKaplansky/Parameters.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.sourceM line 8

    Also declared: ComparatorChallenges/OddKaplansky.lean:7 (same declaration text).

  2. def OAI.OddKaplansky.sourcePrime line 9

    Also declared: ComparatorChallenges/OddKaplansky.lean:8 (same declaration text).

  3. lemma OAI.OddKaplansky.sourceM_large line 11
  4. lemma OAI.OddKaplansky.sourcePrime_prime line 17
  5. lemma OAI.OddKaplansky.sourcePrime_dvd line 24
  6. lemma OAI.OddKaplansky.sourcePrime_gt line 27
  7. lemma OAI.OddKaplansky.sourcePrime_odd line 35
  8. lemma OAI.OddKaplansky.sourcePrime_minimal line 38
  9. instance OAI.OddKaplansky.sourcePrime_fact line 42
  10. lemma OAI.OddKaplansky.neg_one_isSquare_of_dvd line 44
  11. lemma OAI.OddKaplansky.neg_one_isSquare line 52