OAI/Analysis/CharacterCriterion/StandardPrime.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.copies_pos line 40
  2. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.dimension line 43
  3. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.middle_add_one line 47
  4. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.zero_low line 51
  5. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.one_low line 55
  6. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.zero_mid line 59
  7. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.one_mid line 65
  8. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.lower_pos line 71
  9. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.upper_pos line 72
  10. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.next_two line 73
  11. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.size_zero line 77
  12. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.size_succ line 78
  13. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.size_two line 79
  14. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.size_power line 83
  15. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.size_coprime line 87
  16. def OAI.KirchbergRordam.StandardPrimeModel.Algebra line 92
  17. instance OAI.KirchbergRordam.StandardPrimeModel.(instance at line 93) line 93
  18. instance OAI.KirchbergRordam.StandardPrimeModel.(instance at line 94) line 94
  19. instance OAI.KirchbergRordam.StandardPrimeModel.(instance at line 95) line 95
  20. def OAI.KirchbergRordam.StandardPrimeMultiplicity.k₀ line 101
  21. def OAI.KirchbergRordam.StandardPrimeMultiplicity.k₁ line 102
  22. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.k₀_formula line 103
  23. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.next_factors line 108
  24. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.next_coprime line 111
  25. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.multipliers_coprime line 113
  26. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.copies_ge_fourth line 117
  27. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.fourth_large line 123
  28. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.multiplier_growth line 128
  29. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.total_slots line 136
  30. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.zero_remainder_lt line 143
  31. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.one_remainder_lt line 148
  32. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.zero_remainder line 153
  33. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.one_remainder line 159
  34. lemma OAI.KirchbergRordam.StandardPrimeMultiplicity.middle_classical line 166