Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-07 13:09 b9da50ad

View on Github →

feat(ring_theory/*): Various lemmas used to prove classical nullstellensatz (#5632)

Estimated changes

Modified src/field_theory/mv_polynomial.lean

added theorem mv_polynomial.quotient_mk_comp_C_injective

Modified src/ring_theory/ideal/operations.lean

modified theorem ideal.radical_idem

added theorem ideal.ring_equiv.bot_maximal_iff

Modified src/ring_theory/jacobson_ideal.lean

modified theorem ideal.eq_jacobson_iff_Inf_maximal'

modified theorem ideal.eq_jacobson_iff_Inf_maximal

modified theorem ideal.eq_jacobson_iff_not_mem

modified theorem ideal.eq_radical_of_eq_jacobson

modified theorem ideal.jacobson_eq_bot

modified theorem ideal.jacobson_eq_iff_jacobson_quotient_eq_bot

modified theorem ideal.jacobson_eq_self_of_is_maximal

modified theorem ideal.jacobson_eq_top_iff

added theorem ideal.jacobson_idem

added theorem ideal.jacobson_radical_eq_jacobson

modified theorem ideal.le_jacobson

modified theorem ideal.map_jacobson_of_bijective

modified theorem ideal.map_jacobson_of_surjective

modified theorem ideal.mem_jacobson_iff

modified theorem ideal.radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot

modified theorem ideal.radical_le_jacobson

Modified src/ring_theory/polynomial/basic.lean

added theorem mv_polynomial.map_mv_polynomial_eq_eval₂