OAI/NumberTheory/PiExponent/Jets/RectangularCotangent.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponentApprox.TransverseMultiplicity.RectangularRing line 15
  2. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularPositive line 19
  3. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularAugmentationIdeal line 22
  4. def OAI.PiExponentApprox.TransverseMultiplicity.unitRectIndex line 26
  5. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularFirstCoefficients line 34
  6. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularFirstCoefficients_mk line 41
  7. theorem OAI.PiExponentApprox.TransverseMultiplicity.firstCoeff_mul line 48
  8. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangular_reconstruct line 58
  9. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangular_monomial_mem_square line 80
  10. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangular_mem_square_of_first_zero line 112
  11. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularIdealFirstCoefficients line 137
  12. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularIdealFirstCoefficients_mul line 143
  13. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularCotangentFirstCoefficients line 161
  14. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularCotangentFirstCoefficients_toCotangent line 167
  15. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularCotangentFirstCoefficients_injective line 174