OAI/NumberTheory/PiExponent/Jets/CompactJetPolynomial.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.CompactJetPolynomial.center line 16
  2. def OAI.PiExponent.CompactJetPolynomial.coordinates line 18
  3. def OAI.PiExponent.CompactJetPolynomial.powerIdeal line 21
  4. theorem OAI.PiExponent.CompactJetPolynomial.eval_center_inverse line 25
  5. theorem OAI.PiExponent.CompactJetPolynomial.span_coordinates line 38
  6. theorem OAI.PiExponent.CompactJetPolynomial.radical_powerIdeal line 61
  7. def OAI.PiExponent.CompactJetPolynomial.centerPoint line 79
  8. theorem OAI.PiExponent.CompactJetPolynomial.zeroLocus_powerIdeal line 82
  9. theorem OAI.PiExponent.CompactJetPolynomial.zeroLocus_finset_prod_powerIdeal line 88
  10. theorem OAI.PiExponent.CompactJetPolynomial.zeroLocus_prod_powerIdeal line 101
  11. def OAI.PiExponent.CompactJetPolynomial.logPolynomials line 108
  12. theorem OAI.PiExponent.CompactJetPolynomial.logPolynomials_eval_zero line 111
  13. theorem OAI.PiExponent.CompactJetPolynomial.truncatedFormalJet_coordinates line 116
  14. theorem OAI.PiExponent.CompactJetPolynomial.map_powerIdeal_truncatedFormalJet line 125
  15. theorem OAI.PiExponent.CompactJetPolynomial.map_powerIdeal_pow_truncatedFormalJet line 138
  16. theorem OAI.PiExponent.CompactJetPolynomial.truncatedFormalJet_mem_weighted_of_mem_pow line 145
  17. theorem OAI.PiExponent.CompactJetPolynomial.formalJet_mem_weighted_of_mem_pow line 155
  18. theorem OAI.PiExponent.CompactJetPolynomial.formalJet_packet_zero_of_mem_pow line 168
  19. theorem OAI.PiExponent.CompactJetPolynomial.aeval_coordinates line 177
  20. theorem OAI.PiExponent.CompactJetPolynomial.map_powerIdeal_aeval line 190