OAI/NumberTheory/PiExponent/Jets/AlgebraicJetPackets.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.AlgebraicJetPackets.triangularMap line 12
  2. def OAI.PiExponent.AlgebraicJetPackets.inverseTriangularMap line 17
  3. theorem OAI.PiExponent.AlgebraicJetPackets.triangularMap_X_zero line 22
  4. theorem OAI.PiExponent.AlgebraicJetPackets.triangularMap_X_succ line 25
  5. theorem OAI.PiExponent.AlgebraicJetPackets.inverseTriangularMap_X_zero line 30
  6. theorem OAI.PiExponent.AlgebraicJetPackets.inverseTriangularMap_X_succ line 33
  7. theorem OAI.PiExponent.AlgebraicJetPackets.triangularMap_comp_inverse line 39
  8. theorem OAI.PiExponent.AlgebraicJetPackets.inverseTriangularMap_comp line 52
  9. def OAI.PiExponent.AlgebraicJetPackets.triangularEquiv line 64
  10. theorem OAI.PiExponent.AlgebraicJetPackets.liftSeries_polynomial line 69
  11. theorem OAI.PiExponent.AlgebraicJetPackets.truncatedFormalJet_eq_polynomial line 80
  12. theorem OAI.PiExponent.AlgebraicJetPackets.truncatedFormalJet_inverse line 100
  13. theorem OAI.PiExponent.AlgebraicJetPackets.quotient_surjective_of_packet line 111
  14. def OAI.PiExponent.AlgebraicJetPackets.algebraicJetMap line 124
  15. def OAI.PiExponent.AlgebraicJetPackets.algebraicJetIdeal line 131
  16. theorem OAI.PiExponent.AlgebraicJetPackets.mem_algebraicJetIdeal line 136
  17. theorem OAI.PiExponent.AlgebraicJetPackets.truncatedFormalJet_packet_surjective line 144
  18. theorem OAI.PiExponent.AlgebraicJetPackets.algebraicJetMap_surjective line 153
  19. def OAI.PiExponent.AlgebraicJetPackets.algebraicJetQuotientEquiv line 159
  20. theorem OAI.PiExponent.AlgebraicJetPackets.algebraicJetQuotientEquiv_mk line 165
  21. theorem OAI.PiExponent.AlgebraicJetPackets.independent_truncatedFormalJet_packets_surjective line 172
  22. theorem OAI.PiExponent.AlgebraicJetPackets.formalJet_packet_surjective line 181