Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-23 20:16 198cb64d

View on Github →

refactor(ring_theory): generalize basic API of ring_hom to ring_hom_class (#14756) This PR generalizes part of the basic API of ring homs to ring_hom_class. This notably includes things like ring_hom.ker, ideal.map and ideal.comap. I left the namespaces unchanged, for example ring_hom.ker remains the same even though it is now defined for any ring_hom_class morphism; this way dot notation still (mostly) works for actual ring homs.

Estimated changes

modified theorem ideal.apply_coe_mem_map
modified theorem ideal.ker_le_comap
modified theorem ideal.map_Inf
modified theorem ideal.map_eq_bot_iff_le_ker
modified theorem ideal.map_is_prime_of_equiv
modified theorem ideal.map_span
modified theorem ideal.mem_map_of_mem
modified theorem ring_hom.comap_ker
modified theorem ring_hom.ker_coe_equiv
modified theorem ring_hom.ker_eq_comap_bot
added theorem ring_hom.ker_equiv
modified theorem ring_hom.ker_is_prime
modified theorem ring_hom.ker_ne_top
modified theorem ring_hom.not_one_mem_ker
modified theorem mv_polynomial.ker_map