OAI/NumberTheory/Catalan/Arithmetic/OddPrimeWeight.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.oddPrimeWeight line 21
  2. theorem OAI.InternalCatalan.one_sub_X_sq_pow_expansion line 23
  3. theorem OAI.InternalCatalan.one_sub_X_sq_pow_coeff_even line 39
  4. theorem OAI.InternalCatalan.one_sub_X_sq_pow_coeff_odd line 54
  5. theorem OAI.InternalCatalan.oddPrimeWeight_coeff_even line 63
  6. theorem OAI.InternalCatalan.oddPrimeWeight_coeff_odd line 68
  7. theorem OAI.InternalCatalan.oddPrimeWeight_coeff_eq_zero_of_ge line 72
  8. theorem OAI.InternalCatalan.one_sub_X_sq_pow_coeff_reverse line 81
  9. theorem OAI.InternalCatalan.oddPrimeWeight_coeff_reverse line 110
  10. theorem OAI.InternalCatalan.oddPrimeWeight_four_ne_zero line 119
  11. theorem OAI.InternalCatalan.oddPrimeWeight_four_pow_ne_zero line 131
  12. theorem OAI.InternalCatalan.oddPrimeWeight_centralCoeff_mul_identity line 136
  13. theorem OAI.InternalCatalan.oddPrimeWeight_centralCoeff_identity line 196
  14. theorem OAI.InternalCatalan.oddPrimeWeight_four_pow_isUnit line 203
  15. theorem OAI.InternalCatalan.oddPrimeWeight_coeff_central line 208
  16. theorem OAI.InternalCatalan.oddPrimeWeight_coeff_of_lt line 215