OAI/NumberTheory/PiExponent/Jets/TransverseMultiplicity.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentApprox.TransverseMultiplicity.RectIndex line 20
  2. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularIdeal line 22
  3. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularPacket line 42
  4. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularPacket_surjective line 49
  5. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularQuotientCoefficients line 61
  6. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularQuotientCoefficients_mk line 71
  7. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularQuotientCoefficients_bijective line 76
  8. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularQuotientEquiv line 91
  9. def OAI.PiExponentApprox.TransverseMultiplicity.rectIndexEquiv line 96
  10. instance OAI.PiExponentApprox.TransverseMultiplicity.rectIndexFintype line 109
  11. theorem OAI.PiExponentApprox.TransverseMultiplicity.card_rectIndex line 112
  12. instance OAI.PiExponentApprox.TransverseMultiplicity.rectangularQuotientFinite line 116
  13. theorem OAI.PiExponentApprox.TransverseMultiplicity.finrank_rectangularQuotient line 120
  14. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularAugmentation line 125
  15. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularAugmentation_mk line 134
  16. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularAugmentation_algebraMap line 140
  17. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularQuotient_isLocal line 147
  18. theorem OAI.PiExponentApprox.TransverseMultiplicity.ordinaryIdeal_le_rectangularIdeal line 153
  19. theorem OAI.PiExponentApprox.TransverseMultiplicity.ordinaryOneIdeal_eq_constantKernel line 164
  20. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularAugmentation_ker_eq_map line 172
  21. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularAugmentation_ker_pow line 184
  22. theorem OAI.PiExponentApprox.TransverseMultiplicity.length_rectangularQuotient line 200
  23. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularTaylorFactor line 209
  24. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularTaylorFactor_mk line 218
  25. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangular_length_le_of_residue_cotangent line 224
  26. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangular_quotient_length_le_of_residue_cotangent line 243
  27. def OAI.PiExponentApprox.TransverseMultiplicity.rectangularTaylorAlgHom line 274
  28. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularTaylorAlgHom_apply line 280
  29. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularTaylorAlgHom_augmentation line 287
  30. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularTaylorAlgHom_maps_residueIdeal line 297
  31. theorem OAI.PiExponentApprox.TransverseMultiplicity.rectangularTaylor_length_lower line 309
  32. def OAI.PiExponentApprox.TransverseMultiplicity.localizedTaylorMap line 329
  33. theorem OAI.PiExponentApprox.TransverseMultiplicity.localizedTaylorMap_algebraMap line 340
  34. theorem OAI.PiExponentApprox.TransverseMultiplicity.localizedTaylorMap_constant line 349
  35. theorem OAI.PiExponentApprox.TransverseMultiplicity.linearCoefficient_mul line 362
  36. theorem OAI.PiExponentApprox.TransverseMultiplicity.localizedTaylorMap_linearCoefficient line 374
  37. theorem OAI.PiExponentApprox.TransverseMultiplicity.localizedTaylorMap_ideal_le line 403
  38. def OAI.PiExponentApprox.TransverseMultiplicity.localizedRectangularTaylorFactor line 418
  39. theorem OAI.PiExponentApprox.TransverseMultiplicity.localizedRectangularTaylorFactor_mk line 432