OAI/NumberTheory/PiExponent/Polynomials/PolynomialLocalUnmixedness.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentJets.PolynomialLocalUnmixedness.pairRelation line 18
  2. def OAI.PiExponentJets.PolynomialLocalUnmixedness.pairBoundary line 23
  3. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.regular_pair_components line 28
  4. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.regular_pair_syzygy line 39
  5. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.regular_pair_range_boundary_eq_kernel line 56
  6. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.regular_pair_boundary_injective line 69
  7. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.pair_relation_range line 76
  8. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.pair_relation_range_eq_quotient_kernel line 92
  9. def OAI.PiExponentJets.PolynomialLocalUnmixedness.pairToIdeal line 96
  10. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.pairToIdeal_surjective line 101
  11. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.regular_pair_range_boundary_eq_kernel_toIdeal line 109
  12. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.ideal_subtype_range_eq_quotient_kernel line 115
  13. abbrev OAI.PiExponentJets.PolynomialLocalUnmixedness.PolynomialLocal line 125
  14. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.polynomial_local_regular_pair_resolution line 127
  15. theorem OAI.PiExponentJets.PolynomialLocalUnmixedness.polynomial_local_regular_pair_dimension_drop line 138
  16. def OAI.PiExponentJets.PolynomialLocalUnmixedness.PolynomialLocalPairUnmixednessTarget line 145