OAI/RingTheory/DirectFiniteness/PrescribedParameters.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyCounterexample.Prescription.Qcard line 9
  2. lemma OAI.KaplanskyCounterexample.Prescription.prime_exists line 11
  3. def OAI.KaplanskyCounterexample.Prescription.prime line 23
  4. def OAI.KaplanskyCounterexample.Prescription.degree line 24
  5. def OAI.KaplanskyCounterexample.Prescription.exponent line 25
  6. def OAI.KaplanskyCounterexample.Prescription.blockdim line 26
  7. def OAI.KaplanskyCounterexample.Prescription.dimension line 27
  8. lemma OAI.KaplanskyCounterexample.Prescription.prime_prime line 29
  9. lemma OAI.KaplanskyCounterexample.Prescription.prime_congruent line 30
  10. lemma OAI.KaplanskyCounterexample.Prescription.prime_le line 32
  11. lemma OAI.KaplanskyCounterexample.Prescription.prime_pos line 34
  12. lemma OAI.KaplanskyCounterexample.Prescription.prime_ge line 35
  13. lemma OAI.KaplanskyCounterexample.Prescription.prime_odd line 42
  14. lemma OAI.KaplanskyCounterexample.Prescription.dimension_pos line 44
  15. lemma OAI.KaplanskyCounterexample.Prescription.prime_217 line 48
  16. lemma OAI.KaplanskyCounterexample.Prescription.degree_217 line 52
  17. lemma OAI.KaplanskyCounterexample.Prescription.dimension_217 line 54