OAI/Algebra/OddKaplansky/SourceFit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.SourceFit.Slot line 18
  2. def OAI.OddKaplansky.SourceFit.polynomial line 19
  3. def OAI.OddKaplansky.SourceFit.alpha line 22
  4. def OAI.OddKaplansky.SourceFit.beta line 23
  5. def OAI.OddKaplansky.SourceFit.fitting line 25
  6. lemma OAI.OddKaplansky.SourceFit.fitting_eq line 27
  7. lemma OAI.OddKaplansky.SourceFit.denominator line 36
  8. lemma OAI.OddKaplansky.SourceFit.fitting_diagonal line 51
  9. lemma OAI.OddKaplansky.SourceFit.intersection_lt line 58
  10. lemma OAI.OddKaplansky.SourceFit.fitting_nonedge line 68
  11. lemma OAI.OddKaplansky.SourceFit.card_slots line 82
  12. lemma OAI.OddKaplansky.SourceFit.ratio_bound line 86