Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-11 09:26 da420a8c

View on Github →

refactor(*): reduce dependencies on ring_theory.ideal.quotient_operations (#18530)

Estimated changes

Modified src/data/polynomial/div.lean

deleted theorem polynomial.quotient_span_X_sub_C_alg_equiv_mk

deleted theorem polynomial.quotient_span_X_sub_C_alg_equiv_symm_apply

Modified src/data/zmod/quotient.lean

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

Modified src/number_theory/multiplicity.lean

Modified src/ring_theory/adjoin_root.lean

Modified src/ring_theory/eisenstein_criterion.lean

Modified src/ring_theory/etale.lean

Modified src/ring_theory/finite_presentation.lean

Modified src/ring_theory/jacobson_ideal.lean

Modified src/ring_theory/nilpotent.lean

deleted theorem ideal.is_nilpotent.induction_on

deleted theorem ideal.is_radical_iff_quotient_reduced

deleted theorem is_nilpotent.is_unit_quotient_mk_iff

Modified src/ring_theory/noetherian.lean

Modified src/ring_theory/polynomial/basic.lean

deleted theorem ideal.eq_zero_of_polynomial_mem_map_range

deleted theorem ideal.eval₂_C_mk_eq_zero

deleted theorem ideal.is_domain_map_C_quotient

added theorem ideal.is_prime_map_C_iff_is_prime

deleted def ideal.polynomial_quotient_equiv_quotient_polynomial

deleted theorem ideal.polynomial_quotient_equiv_quotient_polynomial_map_mk

deleted theorem ideal.polynomial_quotient_equiv_quotient_polynomial_symm_mk

deleted theorem ideal.quotient_map_C_eq_zero

deleted theorem mv_polynomial.eval₂_C_mk_eq_zero

deleted def mv_polynomial.quotient_equiv_quotient_mv_polynomial

deleted theorem mv_polynomial.quotient_map_C_eq_zero

Created src/ring_theory/polynomial/quotient.lean

added theorem ideal.eq_zero_of_polynomial_mem_map_range

added theorem ideal.eval₂_C_mk_eq_zero

added theorem ideal.is_domain_map_C_quotient

added def ideal.polynomial_quotient_equiv_quotient_polynomial

added theorem ideal.polynomial_quotient_equiv_quotient_polynomial_map_mk

added theorem ideal.polynomial_quotient_equiv_quotient_polynomial_symm_mk

added theorem ideal.quotient_map_C_eq_zero

added theorem mv_polynomial.eval₂_C_mk_eq_zero

added def mv_polynomial.quotient_equiv_quotient_mv_polynomial

added theorem mv_polynomial.quotient_map_C_eq_zero

added theorem polynomial.quotient_span_X_sub_C_alg_equiv_mk

added theorem polynomial.quotient_span_X_sub_C_alg_equiv_symm_apply

Created src/ring_theory/quotient_nilpotent.lean

added theorem ideal.is_nilpotent.induction_on

added theorem ideal.is_radical_iff_quotient_reduced

added theorem is_nilpotent.is_unit_quotient_mk_iff

Created src/ring_theory/quotient_noetherian.lean

Modified src/ring_theory/valuation/basic.lean

deleted theorem add_valuation.comap_on_quot_eq

deleted theorem add_valuation.comap_supp

deleted def add_valuation.on_quot

deleted theorem add_valuation.on_quot_comap_eq

deleted def add_valuation.on_quot_val

deleted theorem add_valuation.self_le_supp_comap

deleted theorem add_valuation.supp_quot

deleted theorem add_valuation.supp_quot_supp

deleted theorem valuation.comap_on_quot_eq

deleted def valuation.on_quot

deleted theorem valuation.on_quot_comap_eq

deleted def valuation.on_quot_val

deleted theorem valuation.self_le_supp_comap

deleted theorem valuation.supp_quot

deleted theorem valuation.supp_quot_supp

Created src/ring_theory/valuation/quotient.lean

added theorem add_valuation.comap_on_quot_eq

added theorem add_valuation.comap_supp

added def add_valuation.on_quot

added theorem add_valuation.on_quot_comap_eq

added def add_valuation.on_quot_val

added theorem add_valuation.self_le_supp_comap

added theorem add_valuation.supp_quot

added theorem add_valuation.supp_quot_supp

added theorem valuation.comap_on_quot_eq

added def valuation.on_quot

added theorem valuation.on_quot_comap_eq

added def valuation.on_quot_val

added theorem valuation.self_le_supp_comap

added theorem valuation.supp_quot

added theorem valuation.supp_quot_supp