OAI/NumberTheory/SiegelZeros/LocalAlgebra/RegularPrefixLocalization.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pairRelation line 33
  2. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pairBoundary line 38
  3. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.regular_pair_components line 43
  4. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.regular_pair_syzygy line 54
  5. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.regular_pair_range_boundary_eq_kernel line 71
  6. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.regular_pair_boundary_injective line 84
  7. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pair_relation_range line 91
  8. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pair_relation_range_eq_quotient_kernel line 107
  9. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pairToIdeal line 111
  10. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pairToIdeal_surjective line 116
  11. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.regular_pair_range_boundary_eq_kernel_toIdeal line 124
  12. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.ideal_subtype_range_eq_quotient_kernel line 130
  13. abbrev OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.PolynomialLocal line 141
  14. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.polynomial_local_regular_pair_resolution line 143
  15. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.polynomial_local_regular_pair_dimension_drop line 154
  16. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.PolynomialLocalPairUnmixednessTarget line 161
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W18.ext_subsingleton_of_shortExact line 183
  18. theorem OAI.SiegelZeros.WeightedTorusJets.W18.ext_zero_of_finite_exact_resolution line 197
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W18.nonzero_ext_forces_resolution_obstruction line 211
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W18.lengthTwo_ext_zero line 223
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W18.associatedPrime_nonzero_quotient_hom line 241
  22. theorem OAI.SiegelZeros.WeightedTorusJets.W18.associatedPrime_nonzero_ext_zero line 252
  23. theorem OAI.SiegelZeros.WeightedTorusJets.W18.not_isAssociatedPrime_of_ext_zero line 261
  24. theorem OAI.SiegelZeros.WeightedTorusJets.W18.associatedPrime_local_nonzero_ext_zero line 268
  25. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ext_subsingleton_of_finite_identity_factorization line 297
  26. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ext_subsingleton_of_finite_basis line 321
  27. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ext_subsingleton_of_finite_free line 336
  28. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pairQuotientShortComplex line 353
  29. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pairSyzygyShortComplex line 360
  30. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pairQuotientShortComplex_shortExact line 368
  31. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pairSyzygyShortComplex_shortExact line 376
  32. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalUnmixedness.pair_resolution_shortComplex_link line 385
  33. theorem OAI.SiegelZeros.WeightedTorusJets.W18.regular_pair_ext_zero line 400
  34. theorem OAI.SiegelZeros.WeightedTorusJets.W18.regular_pair_associatedPrime_ext_obstruction line 412
  35. theorem OAI.SiegelZeros.W58.weaklyRegular_map_of_flat line 441
  36. theorem OAI.SiegelZeros.W58.regular_map_of_flat_of_mem_maximalIdeal line 448
  37. theorem OAI.SiegelZeros.W58.localized_ideal_eq_map line 467
  38. def OAI.SiegelZeros.W58.localizedIdealQuotientEquiv line 473
  39. theorem OAI.SiegelZeros.W58.associatedPrime_quotient_atPrime line 478
  40. theorem OAI.SiegelZeros.W58.ideal_le_of_quotient_associatedPrime line 488
  41. theorem OAI.SiegelZeros.W58.regular_list_at_associatedPrime line 493
  42. theorem OAI.SiegelZeros.W58.regular_pair_localized_ext_obstruction line 513
  43. theorem OAI.SiegelZeros.WeightedTorusJets.W16.weaklyRegular_atPrime_mono line 541
  44. theorem OAI.SiegelZeros.WeightedTorusJets.W16.regularPrefix_quotientMul_injective line 580