OAI/NumberTheory/PiExponent/Polynomials/PolynomialAssociatedLocalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSiegel.W58.weaklyRegular_map_of_flat line 20
2. theorem OAI.PiExponentSiegel.W58.regular_map_of_flat_of_mem_maximalIdeal line 27
3. theorem OAI.PiExponentSiegel.W58.localized_ideal_eq_map line 46
4. def OAI.PiExponentSiegel.W58.localizedIdealQuotientEquiv line 52
5. theorem OAI.PiExponentSiegel.W58.associatedPrime_quotient_atPrime line 57
6. theorem OAI.PiExponentSiegel.W58.ideal_le_of_quotient_associatedPrime line 67
7. theorem OAI.PiExponentSiegel.W58.regular_list_at_associatedPrime line 72
8. theorem OAI.PiExponentSiegel.W58.regular_pair_localized_ext_obstruction line 91