Commit 2022-12-26 14:51 84ee4ca8

View on Github →

feat: port Algebra.Ring.Equiv (#1077) See discussion here and there I used #835 as a reference

Estimated changes

added theorem RingEquiv.coe_trans
added theorem RingEquiv.comp_symm
added theorem RingEquiv.ext
added theorem RingEquiv.map_neg_one
added theorem RingEquiv.mk_coe'
added theorem RingEquiv.mk_coe
added def RingEquiv.refl
added theorem RingEquiv.refl_apply
added theorem RingEquiv.symm_comp
added theorem RingEquiv.symm_mk
added theorem RingEquiv.symm_symm
added theorem RingEquiv.symm_trans
added theorem RingEquiv.trans_apply
added structure RingEquiv