OAI/NumberTheory/Jacobsthal/Siegel/MonicSMulRegularQuotientMapC.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.monic_isSMulRegular_quotient_map_C line 16
  2. theorem OAI.Erdos970.WeightedTorusJets.exists_regular_generators_polynomial_localization line 32
  3. theorem OAI.Erdos970.WeightedTorusJets.regular_maximal_generators_of_ringEquiv line 82
  4. theorem OAI.Erdos970.WeightedTorusJets.exists_regular_maximal_generators_field_localization line 94
  5. theorem OAI.Erdos970.WeightedTorusJets.exists_regular_maximal_generators_localizations_of_ringEquiv line 105
  6. theorem OAI.Erdos970.WeightedTorusJets.exists_regular_maximal_generators_polynomial_localizations line 123
  7. theorem OAI.Erdos970.WeightedTorusJets.exists_regular_maximal_generators_mvPolynomial_localization line 161
  8. theorem OAI.Erdos970.WeightedTorusJets.span_singleton_sup_eq_of_sub_mem line 187
  9. theorem OAI.Erdos970.WeightedTorusJets.isRegular_append_singleton_iff_sub_mem line 198
  10. theorem OAI.Erdos970.WeightedTorusJets.isRegular_cons_iff_sub_mem line 210
  11. theorem OAI.Erdos970.WeightedTorusJets.exists_regular_sequence_of_mem_sup_annihilator line 219
  12. theorem OAI.Erdos970.WeightedTorusJets.exists_regular_sequence_quotSMulTop_of_mem_sup line 243
  13. theorem OAI.Erdos970.WeightedTorusJets.exists_regular_sequence_quotient_of_regular_element line 264
  14. theorem OAI.Erdos970.WeightedTorusJets.exists_add_not_mem_of_prime_antichain line 301
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_add_not_mem_of_finite_prime line 356
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_add_isSMulRegular line 373
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_add_isSMulRegular_of_exists line 391
  18. theorem OAI.Erdos970.WeightedTorusJets.isRegular_of_exists_regular_sequence_in_ofList line 409
  19. theorem OAI.Erdos970.WeightedTorusJets.exists_regular_sequence_of_le_radical line 457
  20. theorem OAI.Erdos970.WeightedTorusJets.regular_maximal_generators_length line 472
  21. theorem OAI.Erdos970.WeightedTorusJets.isRegular_parameters_of_exists_regular_maximal_generators line 487