OAI/Algebra/OddKaplansky/GraphNumerics.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.GraphNumerics.binomDefinition line 12
  2. opaque OAI.OddKaplansky.GraphNumerics.binomWrapped line 13
  3. def OAI.OddKaplansky.GraphNumerics.binom line 15
  4. theorem OAI.OddKaplansky.GraphNumerics.binom_def line 16
  5. lemma OAI.OddKaplansky.GraphNumerics.choose_mono_small line 23
  6. lemma OAI.OddKaplansky.GraphNumerics.choose_step line 33
  7. lemma OAI.OddKaplansky.GraphNumerics.choose_growth line 43
  8. lemma OAI.OddKaplansky.GraphNumerics.sum_small_bound line 57
  9. lemma OAI.OddKaplansky.GraphNumerics.ratio_bound line 63
  10. lemma OAI.OddKaplansky.GraphNumerics.source_ratio_bound line 75
  11. def OAI.OddKaplansky.GraphNumerics.smallSetEquiv line 80
  12. lemma OAI.OddKaplansky.GraphNumerics.card_small_sets line 92