OAI/NumberTheory/PiExponent/Polynomials/PowerCoverExponents.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.PowerCover.scale line 11
  2. def OAI.PiExponent.PowerCover.quotient line 14
  3. def OAI.PiExponent.PowerCover.residue line 17
  4. def OAI.PiExponent.PowerCover.combine line 21
  5. theorem OAI.PiExponent.PowerCover.scale_apply line 24
  6. theorem OAI.PiExponent.PowerCover.quotient_apply line 27
  7. theorem OAI.PiExponent.PowerCover.residue_apply line 31
  8. theorem OAI.PiExponent.PowerCover.combine_apply line 35
  9. theorem OAI.PiExponent.PowerCover.combine_quotient_residue line 39
  10. theorem OAI.PiExponent.PowerCover.quotient_combine line 46
  11. theorem OAI.PiExponent.PowerCover.residue_combine line 54
  12. def OAI.PiExponent.PowerCover.exponentEquiv line 61
  13. theorem OAI.PiExponent.PowerCover.exponentEquiv_apply line 68
  14. theorem OAI.PiExponent.PowerCover.exponentEquiv_symm_apply line 71
  15. theorem OAI.PiExponent.PowerCover.quotient_add_scale line 75
  16. theorem OAI.PiExponent.PowerCover.residue_add_scale line 82
  17. theorem OAI.PiExponent.PowerCover.exponentEquiv_add_scale line 89
  18. theorem OAI.PiExponent.PowerCover.combine_add line 94
  19. theorem OAI.PiExponent.PowerCover.scale_zero line 100
  20. theorem OAI.PiExponent.PowerCover.scale_add line 104