Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-18 15:07 3ca16d0a

View on Github →

feat(data/equiv): define ring_equiv_class (#11977) This PR applies the morphism class pattern to ring_equiv, producing a new ring_equiv_class extending mul_equiv_class and add_equiv_class. It also provides a ring_equiv_class instance for alg_equivs.

Estimated changes

deleted theorem alg_equiv.bijective
modified theorem alg_equiv.ext
deleted theorem alg_equiv.ext_iff
deleted theorem alg_equiv.injective
deleted theorem alg_equiv.map_add
deleted theorem alg_equiv.map_mul
deleted theorem alg_equiv.map_neg
deleted theorem alg_equiv.map_one
deleted theorem alg_equiv.map_pow
deleted theorem alg_equiv.map_sub
deleted theorem alg_equiv.map_zero
deleted theorem alg_equiv.surjective
added theorem ring_hom.coe_coe
modified theorem ring_equiv.ext
deleted theorem ring_equiv.ext_iff
deleted theorem ring_equiv.map_add
deleted theorem ring_equiv.map_eq_one_iff
deleted theorem ring_equiv.map_mul
modified theorem ring_equiv.map_ne_one_iff
modified theorem ring_equiv.map_ne_zero_iff
deleted theorem ring_equiv.map_neg
deleted theorem ring_equiv.map_one
deleted theorem ring_equiv.map_pow
deleted theorem ring_equiv.map_sub
deleted theorem ring_equiv.map_zero