Commit 2023-02-28 17:47 972a45b7

View on Github →

feat: port Algebra.Algebra.Equiv (#2413)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Equiv.lean

added def AlgEquiv.Simps.apply

added def AlgEquiv.Simps.symmApply

added theorem AlgEquiv.algebraMap_eq_apply

added theorem AlgEquiv.apply_symm_apply

added def AlgEquiv.arrowCongr

added theorem AlgEquiv.arrowCongr_comp

added theorem AlgEquiv.arrowCongr_refl

added theorem AlgEquiv.arrowCongr_symm

added theorem AlgEquiv.arrowCongr_trans

added def AlgEquiv.autCongr

added theorem AlgEquiv.autCongr_refl

added theorem AlgEquiv.autCongr_symm

added theorem AlgEquiv.autCongr_trans

added theorem AlgEquiv.aut_mul

added theorem AlgEquiv.aut_one

added theorem AlgEquiv.coe_algHom

added theorem AlgEquiv.coe_algHom_injective

added theorem AlgEquiv.coe_algHom_ofAlgHom

added theorem AlgEquiv.coe_apply_coe_coe_symm_apply

added theorem AlgEquiv.coe_coe_symm_apply_coe_apply

added theorem AlgEquiv.coe_fun_injective

added theorem AlgEquiv.coe_mk

added theorem AlgEquiv.coe_ofBijective

added theorem AlgEquiv.coe_refl

added theorem AlgEquiv.coe_ringEquiv

added theorem AlgEquiv.coe_ringEquiv_injective

added theorem AlgEquiv.coe_ringHom_commutes

added theorem AlgEquiv.coe_ring_equiv'

added theorem AlgEquiv.coe_trans

added theorem AlgEquiv.commutes

added theorem AlgEquiv.comp_symm

added theorem AlgEquiv.ext

added theorem AlgEquiv.invFun_eq_symm

added theorem AlgEquiv.leftInverse_symm

added theorem AlgEquiv.map_finsupp_sum

added theorem AlgEquiv.map_smul

added theorem AlgEquiv.map_sum

added theorem AlgEquiv.mk_coe'

added theorem AlgEquiv.mk_coe

added theorem AlgEquiv.mul_apply

added def AlgEquiv.ofAlgHom

added theorem AlgEquiv.ofAlgHom_coe_algHom

added theorem AlgEquiv.ofAlgHom_symm

added theorem AlgEquiv.ofBijective_apply

added def AlgEquiv.ofLinearEquiv

added theorem AlgEquiv.ofLinearEquiv_symm

added theorem AlgEquiv.ofLinearEquiv_toLinearEquiv

added def AlgEquiv.ofRingEquiv

added theorem AlgEquiv.one_apply

added def AlgEquiv.refl

added theorem AlgEquiv.refl_symm

added theorem AlgEquiv.refl_to_algHom

added theorem AlgEquiv.rightInverse_symm

added def AlgEquiv.symm

added theorem AlgEquiv.symm_apply_apply

added theorem AlgEquiv.symm_bijective

added theorem AlgEquiv.symm_comp

added theorem AlgEquiv.symm_mk

added theorem AlgEquiv.symm_symm

added theorem AlgEquiv.symm_toEquiv_eq_symm

added theorem AlgEquiv.symm_to_ringEquiv

added theorem AlgEquiv.symm_trans_apply

added def AlgEquiv.toAlgHom

added theorem AlgEquiv.toAlgHom_eq_coe

added def AlgEquiv.toLinearEquiv

added theorem AlgEquiv.toLinearEquiv_apply

added theorem AlgEquiv.toLinearEquiv_injective

added theorem AlgEquiv.toLinearEquiv_ofLinearEquiv

added theorem AlgEquiv.toLinearEquiv_refl

added theorem AlgEquiv.toLinearEquiv_symm

added theorem AlgEquiv.toLinearEquiv_toLinearMap

added theorem AlgEquiv.toLinearEquiv_trans

added def AlgEquiv.toLinearMap

added theorem AlgEquiv.toLinearMap_apply

added theorem AlgEquiv.toLinearMap_injective

added theorem AlgEquiv.toRingEquiv_eq_coe

added theorem AlgEquiv.to_algHom_toLinearMap

added theorem AlgEquiv.to_ringEquiv_symm

added def AlgEquiv.trans

added theorem AlgEquiv.trans_apply

added theorem AlgEquiv.trans_toLinearMap

added structure AlgEquiv

added def MulSemiringAction.toAlgEquiv

added theorem MulSemiringAction.toAlgEquiv_injective