OAI/NumberTheory/PiExponent/Analysis/FormalLogTruncation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.FormalLogTruncation.liftSeries_eq_toMvPowerSeries line 15
  2. def OAI.PiExponent.FormalLogTruncation.shiftVars line 45
  3. theorem OAI.PiExponent.FormalLogTruncation.shiftVars_hasSubst line 49
  4. def OAI.PiExponent.FormalLogTruncation.shiftMap line 60
  5. theorem OAI.PiExponent.FormalLogTruncation.shiftMap_X_zero line 65
  6. theorem OAI.PiExponent.FormalLogTruncation.shiftMap_X_succ line 71
  7. theorem OAI.PiExponent.FormalLogTruncation.shiftMap_toMvPowerSeries line 77
  8. theorem OAI.PiExponent.FormalLogTruncation.shiftMap_liftSeries line 84
  9. theorem OAI.PiExponent.FormalLogTruncation.shiftMap_apply line 89
  10. theorem OAI.PiExponent.FormalLogTruncation.shiftMap_inverse line 93
  11. def OAI.PiExponent.FormalLogTruncation.shiftEquiv line 112
  12. theorem OAI.PiExponent.FormalLogTruncation.shiftEquiv_apply line 124
  13. theorem OAI.PiExponent.FormalLogTruncation.rationalWeightedIdeal_prod line 130
  14. theorem OAI.PiExponent.FormalLogTruncation.subst_mem_rationalWeightedIdeal line 146
  15. theorem OAI.PiExponent.FormalLogTruncation.X_mem_rationalWeightedIdeal line 171
  16. theorem OAI.PiExponent.FormalLogTruncation.shiftMap_mem_rationalWeightedIdeal line 182
  17. theorem OAI.PiExponent.FormalLogTruncation.rationalCoefficientPacket_eq_iff line 196
  18. theorem OAI.PiExponent.FormalLogTruncation.rationalCoefficientPacket_surjective line 207
  19. theorem OAI.PiExponent.FormalLogTruncation.packet_surjective_comp_equiv line 215
  20. theorem OAI.PiExponent.FormalLogTruncation.packet_surjective_comp_equiv_iff line 229
  21. theorem OAI.PiExponent.FormalLogTruncation.shiftEquiv_symm_apply line 243
  22. theorem OAI.PiExponent.FormalLogTruncation.shiftEquiv_mem_iff line 248
  23. def OAI.PiExponent.FormalLogTruncation.logTail line 269
  24. theorem OAI.PiExponent.FormalLogTruncation.logTail_constantCoeff line 272
  25. theorem OAI.PiExponent.FormalLogTruncation.coeff_logTail_eq_zero line 276
  26. theorem OAI.PiExponent.FormalLogTruncation.logTail_mem_rationalWeightedIdeal line 280
  27. def OAI.PiExponent.FormalLogTruncation.truncatedFormalJet line 302
  28. theorem OAI.PiExponent.FormalLogTruncation.shiftMap_truncatedFormalJet line 308
  29. theorem OAI.PiExponent.FormalLogTruncation.packets_surjective_comp_equiv line 331
  30. theorem OAI.PiExponent.FormalLogTruncation.packets_surjective_comp_equiv_iff line 347
  31. theorem OAI.PiExponent.FormalLogTruncation.formalLog_packets_surjective_iff_truncated line 361