OAI/NumberTheory/SiegelZeros/LocalAlgebra/MonicSMulRegularQuotientMapC.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.monic_isSMulRegular_quotient_map_C line 13
  2. theorem OAI.SiegelZeros.WeightedTorusJets.exists_regular_generators_polynomial_localization line 29
  3. theorem OAI.SiegelZeros.WeightedTorusJets.regular_maximal_generators_of_ringEquiv line 79
  4. theorem OAI.SiegelZeros.WeightedTorusJets.exists_regular_maximal_generators_field_localization line 91
  5. theorem OAI.SiegelZeros.WeightedTorusJets.exists_regular_maximal_generators_localizations_of_ringEquiv line 102
  6. theorem OAI.SiegelZeros.WeightedTorusJets.exists_regular_maximal_generators_polynomial_localizations line 120
  7. theorem OAI.SiegelZeros.WeightedTorusJets.exists_regular_maximal_generators_mvPolynomial_localization line 158
  8. theorem OAI.SiegelZeros.WeightedTorusJets.span_singleton_sup_eq_of_sub_mem line 184
  9. theorem OAI.SiegelZeros.WeightedTorusJets.isRegular_append_singleton_iff_sub_mem line 195
  10. theorem OAI.SiegelZeros.WeightedTorusJets.isRegular_cons_iff_sub_mem line 207
  11. theorem OAI.SiegelZeros.WeightedTorusJets.exists_regular_sequence_of_mem_sup_annihilator line 216
  12. theorem OAI.SiegelZeros.WeightedTorusJets.exists_regular_sequence_quotSMulTop_of_mem_sup line 240
  13. theorem OAI.SiegelZeros.WeightedTorusJets.exists_regular_sequence_quotient_of_regular_element line 261
  14. theorem OAI.SiegelZeros.WeightedTorusJets.exists_add_not_mem_of_prime_antichain line 298
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_add_not_mem_of_finite_prime line 353
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_add_isSMulRegular line 370
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_add_isSMulRegular_of_exists line 388
  18. theorem OAI.SiegelZeros.WeightedTorusJets.isRegular_of_exists_regular_sequence_in_ofList line 406
  19. theorem OAI.SiegelZeros.WeightedTorusJets.exists_regular_sequence_of_le_radical line 454
  20. theorem OAI.SiegelZeros.WeightedTorusJets.regular_maximal_generators_length line 469
  21. theorem OAI.SiegelZeros.WeightedTorusJets.isRegular_parameters_of_exists_regular_maximal_generators line 484