OAI/NumberTheory/SiegelZeros/LocalAlgebra/RegularParameterSelectionLemmas.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.RegularSequenceQuotientTail.principal_image_eq_scalar_top line 31
  2. def OAI.SiegelZeros.WeightedTorusJets.RegularSequenceQuotientTail.quotientTailEquiv line 37
  3. theorem OAI.SiegelZeros.WeightedTorusJets.RegularSequenceQuotientTail.quotientTailEquiv_mk line 42
  4. theorem OAI.SiegelZeros.WeightedTorusJets.RegularSequenceQuotientTail.regular_quotient_cons_iff line 46
  5. theorem OAI.SiegelZeros.WeightedTorusJets.RegularSequenceQuotientTail.regular_quotient_tail line 53
  6. theorem OAI.SiegelZeros.WeightedTorusJets.RegularSequenceQuotientTail.weaklyRegular_quotient_tail line 58
  7. theorem OAI.SiegelZeros.WeightedTorusJets.RegularSequenceQuotientTail.regular_map_quotient_iff line 64
  8. theorem OAI.SiegelZeros.WeightedTorusJets.RegularSequenceQuotientTail.regular_mapped_quotient_tail line 75
  9. def OAI.SiegelZeros.SiegelZerosAwei.W31.projectiveResolutionOfExact line 96
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.projectiveResolutionOfExact_complex line 115
  11. def OAI.SiegelZeros.SiegelZerosAwei.W31.resolutionExtAddEquiv line 124
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ext_subsingleton_iff_cocycles_are_boundaries line 130
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.ext_subsingleton_of_isZero_resolution_term line 146
  14. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.module_exactAt_succ_of_range_eq_ker line 160
  15. def OAI.SiegelZeros.SiegelZerosAwei.W31.finiteFreeResolutionOfExact line 168
  16. def OAI.SiegelZeros.SiegelZerosAwei.W31.moduleFreeResolutionOfExact line 182
  17. def OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceAugmentation line 209
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceAugmentation_spec line 214
  19. def OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceResolution line 223
  20. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceResolution_complex line 237
  21. def OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceQuotientExtAddEquiv line 241
  22. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceQuotientExt_iff_boundaries line 249
  23. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceQuotientExt_above_length line 258
  24. theorem OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceQuotientExt_of_dual_exact line 266
  25. def OAI.SiegelZeros.SiegelZerosAwei.W31.residueFieldExtAddEquiv line 283
  26. def OAI.SiegelZeros.WeightedTorusJets.W18.differentialRangeShortComplex line 307
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W18.differentialRangeShortComplex_shortExact line 315
  28. def OAI.SiegelZeros.WeightedTorusJets.W18.augmentationRangeShortComplex line 326
  29. theorem OAI.SiegelZeros.WeightedTorusJets.W18.augmentationRangeShortComplex_shortExact line 333
  30. theorem OAI.SiegelZeros.WeightedTorusJets.W18.ext_subsingleton_of_subsingleton_module line 346
  31. def OAI.SiegelZeros.WeightedTorusJets.W18.regularSequenceDifferentialRange line 359
  32. theorem OAI.SiegelZeros.WeightedTorusJets.W18.regularSequenceDifferentialRange_top_subsingleton line 362
  33. theorem OAI.SiegelZeros.WeightedTorusJets.W18.regular_sequence_ext_zero line 372
  34. theorem OAI.SiegelZeros.WeightedTorusJets.W18.regular_sequence_associatedPrime_ext_obstruction line 408
  35. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.iterateScalarCones_dual_low_exact line 434
  36. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.regularSequenceComplex_dual_low_exact line 478
  37. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.regularSequenceQuotientExt_positive_below_length line 520
  38. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.regularSequenceQuotientExt_zero line 526
  39. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.regularSequenceQuotientExt_below_length line 534
  40. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.residueFieldExt_below_regular_length line 544
  41. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.polynomialLocal_residueExt_below_height line 558
  42. theorem OAI.SiegelZeros.W58.polynomialLocal_regular_prefix_maximal_not_associated line 583
  43. theorem OAI.SiegelZeros.W58.polynomialLocal_exists_constant_regular_parameters line 604
  44. theorem OAI.SiegelZeros.W58.polynomialLocal_exists_constant_regular_parameters_actual_height line 625
  45. theorem OAI.SiegelZeros.W58.polynomialLocal_exists_degree_bounded_regular_parameters line 641