Commit 2020-11-23 19:56 fee93e96

View on Github →

feat(ring_theory/*): Various lemmas about ideals, quotients, and localizations (#5046) Lemmas needed for the proof that is_jacobson is preserved under taking polynomials.

Estimated changes

Modified src/data/polynomial/eval.lean

added theorem polynomial.coe_map_ring_hom

added theorem polynomial.eval₂_C_X

modified theorem polynomial.map_injective

added def polynomial.map_ring_hom

added theorem polynomial.map_surjective

Modified src/group_theory/submonoid/operations.lean

modified theorem submonoid.mem_map_of_mem

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.bot_quotient_is_maximal_iff

added theorem ideal.comp_quotient_map_eq_of_comp_eq

added theorem ideal.quotient_map_injective

added theorem ideal.quotient_map_mk

added theorem ideal.radical_bot_of_integral_domain

Modified src/ring_theory/ideal/over.lean

added theorem ideal.is_maximal_comap_of_is_integral_of_is_maximal'

added theorem ideal.is_maximal_of_is_integral_of_is_maximal_comap'

Modified src/ring_theory/integral_closure.lean

added theorem is_integral_of_is_integral_mul_unit'

added theorem is_integral_of_mem_closure''

added theorem is_integral_of_mem_closure'

added theorem is_integral_of_surjective'

added theorem is_integral_quotient_of_is_integral'

added theorem is_integral_tower_bot_of_is_integral'

added theorem ring_hom.is_integral_trans

Modified src/ring_theory/localization.lean

added theorem is_integral_elem_localization_at_leading_coeff'

added theorem is_integral_localization'

added theorem localization_map.surjective_quotient_map_of_maximal_of_localization

Modified src/ring_theory/non_zero_divisors.lean

added theorem map_le_non_zero_divisors_of_injective

added theorem powers_le_non_zero_divisors_of_domain

Modified src/ring_theory/polynomial/basic.lean

added theorem ideal.eq_zero_of_polynomial_mem_map_range

added theorem ideal.polynomial_mem_ideal_of_coeff_mem_ideal

modified def ideal.polynomial_quotient_equiv_quotient_polynomial