OAI/NumberTheory/SiegelZeros/LocalAlgebra/RegularParameterSelection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.W20.regular_sequence_ideal_ne_top line 24
2. theorem OAI.SiegelZeros.W20.regular_sequence_term_not_isUnit line 32
3. theorem OAI.SiegelZeros.W20.regular_sequence_term_ne_zero line 40
4. theorem OAI.SiegelZeros.W20.regular_homogeneous_degrees_pos line 62
5. theorem OAI.SiegelZeros.W20.regular_homogeneous_degree_product_ne_zero line 83
6. theorem OAI.SiegelZeros.W58.isSMulRegular_of_avoids_associatedPrimes line 106
7. theorem OAI.SiegelZeros.W58.regular_append_singleton_of_quotient_smulRegular line 121
8. theorem OAI.SiegelZeros.W58.exists_constant_regular_extension line 143
9. theorem OAI.SiegelZeros.W58.regular_full_length_radical_eq_maximalIdeal line 192
10. theorem OAI.SiegelZeros.W58.constant_linearCombination_mem_ideal line 218
11. theorem OAI.SiegelZeros.W58.exists_constant_regular_parameters_of_no_maximal_associated line 227