OAI/NumberTheory/PiExponent/Jets/AffineJetPackets.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.AffineJetPackets.formalJet_packet_eq_of_sub_mem_pow line 14
  2. theorem OAI.PiExponent.AffineJetPackets.formalJet_packets_surjective line 27
  3. theorem OAI.PiExponent.AffineJetPackets.packets_surjective_of_polynomialIdeal_quotient line 47