Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-30 10:52 9f955fe5

View on Github →

feat(ring_theory/integral_closure): Cleanup interface for ring_hom.is_integral (#5144)

Estimated changes

Modified src/ring_theory/integral_closure.lean

deleted theorem is_integral_of_is_integral_mul_unit'

deleted theorem is_integral_of_surjective'

deleted theorem is_integral_quotient_of_is_integral'

deleted theorem is_integral_tower_bot_of_is_integral'

added theorem ring_hom.is_integral_add

added theorem ring_hom.is_integral_map

added theorem ring_hom.is_integral_mul

added theorem ring_hom.is_integral_neg

added theorem ring_hom.is_integral_of_is_integral_mul_unit

added theorem ring_hom.is_integral_of_mem_closure

added theorem ring_hom.is_integral_of_surjective

added theorem ring_hom.is_integral_one

added theorem ring_hom.is_integral_quotient_of_is_integral

added theorem ring_hom.is_integral_sub

added theorem ring_hom.is_integral_tower_bot_of_is_integral

modified theorem ring_hom.is_integral_trans

added theorem ring_hom.is_integral_zero

Modified src/ring_theory/jacobson.lean

Modified src/ring_theory/localization.lean

deleted theorem is_integral_elem_localization_at_leading_coeff'

added theorem ring_hom.is_integral_elem_localization_at_leading_coeff