Commit 2022-12-06 23:13 a2d57a97

View on Github →

feat: port Algebra.Hom.Equiv.Basic (#835) mathlib3 SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Hom/Equiv/Basic.lean

added structure AddEquiv

added theorem Equiv.inv_symm

added def MonoidHom.inverse

added def MonoidHom.toMulEquiv

added def MulEquiv.Simps.symmApply

added theorem MulEquiv.apply_eq_iff_eq

added theorem MulEquiv.apply_eq_iff_symm_apply

added theorem MulEquiv.apply_symm_apply

added def MulEquiv.arrowCongr

added theorem MulEquiv.coe_monoidHom_refl

added theorem MulEquiv.coe_monoidHom_trans

added theorem MulEquiv.coe_refl

added theorem MulEquiv.coe_toMulHom

added theorem MulEquiv.coe_to_monoidHom

added theorem MulEquiv.coe_trans

added theorem MulEquiv.comp_symm_eq

added theorem MulEquiv.eq_comp_symm

added theorem MulEquiv.eq_symm_apply

added theorem MulEquiv.eq_symm_comp

added theorem MulEquiv.ext

added theorem MulEquiv.ext_iff

added theorem MulEquiv.invFun_eq_symm

added theorem MulEquiv.map_ne_one_iff

added def MulEquiv.mk'

added theorem MulEquiv.mk_coe'

added theorem MulEquiv.mk_coe

added def MulEquiv.monoidHomCongr

added def MulEquiv.mulEquivOfUnique

added theorem MulEquiv.ofBijective_apply_symm_apply

added def MulEquiv.piCongrRight

added theorem MulEquiv.piCongrRight_refl

added theorem MulEquiv.piCongrRight_symm

added theorem MulEquiv.piCongrRight_trans

added def MulEquiv.piSubsingleton

added def MulEquiv.refl

added theorem MulEquiv.refl_apply

added theorem MulEquiv.refl_symm

added theorem MulEquiv.self_comp_symm

added theorem MulEquiv.self_trans_symm

added def MulEquiv.symm

added theorem MulEquiv.symm_apply_apply

added theorem MulEquiv.symm_apply_eq

added theorem MulEquiv.symm_bijective

added theorem MulEquiv.symm_comp_eq

added theorem MulEquiv.symm_comp_self

added theorem MulEquiv.symm_mk

added theorem MulEquiv.symm_symm

added theorem MulEquiv.symm_trans_apply

added theorem MulEquiv.symm_trans_self

added theorem MulEquiv.toEquiv_symm

added def MulEquiv.toMonoidHom

added theorem MulEquiv.to_monoidHom_injective

added def MulEquiv.trans

added theorem MulEquiv.trans_apply

added structure MulEquiv

added theorem MulEquivClass.map_eq_one_iff

added theorem MulEquivClass.map_ne_one_iff

added def MulHom.inverse

added def MulHom.toMulEquiv

Modified Mathlib/Algebra/Hom/Group.lean

deleted theorem map_zsmul'

Modified Mathlib/Algebra/Hom/Units.lean

Modified Mathlib/Logic/Function/Basic.lean