Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-12 07:16 0344aeed

View on Github →

feat(ring_theory/*): various lemmas about quotients, localizations, and polynomials (#5249)

Estimated changes

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.quotient_map_comp_mk

added theorem ideal.quotient_map_surjective

Modified src/ring_theory/integral_closure.lean

added theorem is_integral_quotient_map_iff

added theorem ring_hom.is_integral_elem_of_is_integral_elem_comp

added theorem ring_hom.is_integral_tower_top_of_is_integral

Modified src/ring_theory/jacobson.lean

modified theorem ideal.radical_eq_jacobson

Modified src/ring_theory/localization.lean

added theorem localization_map_bijective_of_field

added theorem map_injective_of_injective

Modified src/ring_theory/polynomial/basic.lean

added theorem ideal.eq_zero_of_constant_mem_of_maximal

added theorem ideal.polynomial_not_is_field