Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-26 07:55 a02f11fa

View on Github →

feat(algebra/ring/equiv): generalize ring_equiv material to allow for non-unital rings (#13626)

Estimated changes

Modified src/algebra/hom/equiv.lean

modified theorem mul_equiv.Pi_congr_right_refl

modified def mul_equiv.arrow_congr

Modified src/algebra/ring/equiv.lean

added def add_equiv.to_ring_equiv

modified def mul_equiv.to_ring_equiv

modified theorem ring_equiv.Pi_congr_right_refl

added theorem ring_equiv.coe_non_unital_ring_hom_inj_iff

modified theorem ring_equiv.coe_of_bijective

added theorem ring_equiv.coe_to_non_unital_ring_hom

modified theorem ring_equiv.of_bijective_apply

added def ring_equiv.of_hom_inv'

modified def ring_equiv.of_hom_inv

deleted theorem ring_equiv.of_hom_inv_apply

deleted theorem ring_equiv.of_hom_inv_symm_apply

added theorem ring_equiv.symm_to_non_unital_ring_hom_apply_to_non_unital_ring_hom_apply

added theorem ring_equiv.symm_to_non_unital_ring_hom_comp_to_non_unital_ring_hom

added def ring_equiv.to_non_unital_ring_hom

added theorem ring_equiv.to_non_unital_ring_hom_apply_symm_to_non_unital_ring_hom_apply

added theorem ring_equiv.to_non_unital_ring_hom_commutes

added theorem ring_equiv.to_non_unital_ring_hom_comp_symm_to_non_unital_ring_hom

added theorem ring_equiv.to_non_unital_ring_hom_eq_coe

added theorem ring_equiv.to_non_unital_ring_hom_injective

added theorem ring_equiv.to_non_unital_ring_hom_refl

added theorem ring_equiv.to_non_unital_ring_hom_trans

Modified src/data/polynomial/eval.lean

Modified src/ring_theory/free_comm_ring.lean

Modified src/ring_theory/valuation/valuation_ring.lean