OAI/NumberTheory/PiExponent/Polynomials/GradedLocalizationExact.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.GradedLocalizationExact.powerDenominator line 17
  2. theorem OAI.PiExponent.GradedLocalizationExact.powerDenominator_val line 20
  3. theorem OAI.PiExponent.GradedLocalizationExact.powerDenominator_zero line 23
  4. theorem OAI.PiExponent.GradedLocalizationExact.powerDenominator_add line 27
  5. def OAI.PiExponent.GradedLocalizationExact.fraction line 32
  6. theorem OAI.PiExponent.GradedLocalizationExact.fraction_zero line 35
  7. theorem OAI.PiExponent.GradedLocalizationExact.fraction_neg line 38
  8. theorem OAI.PiExponent.GradedLocalizationExact.fraction_add line 41
  9. theorem OAI.PiExponent.GradedLocalizationExact.fraction_cancel line 47
  10. theorem OAI.PiExponent.GradedLocalizationExact.fraction_eq_zero line 53
  11. theorem OAI.PiExponent.GradedLocalizationExact.power_smul_mem line 71
  12. def OAI.PiExponent.GradedLocalizationExact.degreePiece line 76
  13. theorem OAI.PiExponent.GradedLocalizationExact.mem_degreePiece line 95
  14. def OAI.PiExponent.GradedLocalizationExact.localizedMap line 99
  15. theorem OAI.PiExponent.GradedLocalizationExact.localizedMap_fraction line 104
  16. def OAI.PiExponent.GradedLocalizationExact.pieceMap line 110
  17. theorem OAI.PiExponent.GradedLocalizationExact.pieceMap_coe line 120
  18. theorem OAI.PiExponent.GradedLocalizationExact.preserves_of_compatible line 128
  19. theorem OAI.PiExponent.GradedLocalizationExact.homogeneous_preimage line 137
  20. theorem OAI.PiExponent.GradedLocalizationExact.pieceMap_surjective line 146
  21. theorem OAI.PiExponent.GradedLocalizationExact.pieceMap_exact line 161
  22. theorem OAI.PiExponent.GradedLocalizationExact.exists_exact_localized_free_presentation line 201