OAI/NumberTheory/TotientFibers/FiniteFiber.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TotientFibers.fiber line 9
  2. def OAI.TotientFibers.g line 11
  3. theorem OAI.TotientFibers.preimage_le line 13
  4. theorem OAI.TotientFibers.fiber_finite line 36
  5. theorem OAI.TotientFibers.card_le_g line 41
  6. theorem OAI.TotientFibers.two_le_g_prime_pred line 46
  7. theorem OAI.TotientFibers.totient_large_fibers_of_one_le line 60
  8. theorem OAI.TotientFibers.infinite_of_unbounded_g line 73
  9. theorem OAI.TotientFibers.factorization_le_log line 82
  10. theorem OAI.TotientFibers.card_le_of_smooth line 90
  11. theorem OAI.TotientFibers.prime_prod_eq_iff line 119
  12. theorem OAI.TotientFibers.totient_prime_prod line 129
  13. theorem OAI.TotientFibers.finite_pigeonhole line 136
  14. theorem OAI.TotientFibers.binomial_ge_ratio line 190
  15. theorem OAI.TotientFibers.logarithmic_count_bound line 213
  16. theorem OAI.TotientFibers.finite_large_fiber line 238
  17. theorem OAI.TotientFibers.finite_large_fiber_rpow line 274