Mathlib Changelog
Changelog
About
Github
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