Commit 2023-01-27 06:03 0298ff32

View on Github →

feat : port Algebra.Module.Equiv (#1732)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Equiv.lean

added theorem AddEquiv.coe_toIntLinearEquiv

added theorem AddEquiv.coe_toLinearEquiv

added theorem AddEquiv.coe_toLinearEquiv_symm

added theorem AddEquiv.coe_toNatLinearEquiv

added def AddEquiv.toIntLinearEquiv

added theorem AddEquiv.toIntLinearEquiv_refl

added theorem AddEquiv.toIntLinearEquiv_symm

added theorem AddEquiv.toIntLinearEquiv_toAddEquiv

added theorem AddEquiv.toIntLinearEquiv_trans

added def AddEquiv.toLinearEquiv

added def AddEquiv.toNatLinearEquiv

added theorem AddEquiv.toNatLinearEquiv_refl

added theorem AddEquiv.toNatLinearEquiv_symm

added theorem AddEquiv.toNatLinearEquiv_toAddEquiv

added theorem AddEquiv.toNatLinearEquiv_trans

added def DistribMulAction.toLinearEquiv

added def DistribMulAction.toModuleAut

added def LinearEquiv.Simps.symmApply

added theorem LinearEquiv.apply_symm_apply

added def LinearEquiv.automorphismGroup.toLinearMapMonoidHom

added theorem LinearEquiv.coe_coe

added theorem LinearEquiv.coe_injective

added theorem LinearEquiv.coe_ofInvolutive

added theorem LinearEquiv.coe_symm_mk

added theorem LinearEquiv.coe_toAddEquiv

added theorem LinearEquiv.coe_toEquiv

added theorem LinearEquiv.coe_toEquiv_symm

added theorem LinearEquiv.coe_toLinearMap

added theorem LinearEquiv.coe_trans

added theorem LinearEquiv.comp_coe

added theorem LinearEquiv.comp_symm_eq

added theorem LinearEquiv.comp_toLinearMap_symm_eq

added theorem LinearEquiv.eq_comp_symm

added theorem LinearEquiv.eq_comp_toLinearMap_symm

added theorem LinearEquiv.eq_symm_apply

added theorem LinearEquiv.eq_symm_comp

added theorem LinearEquiv.eq_toLinearMap_symm_comp

added theorem LinearEquiv.ext

added theorem LinearEquiv.ext_iff

added theorem LinearEquiv.invFun_eq_symm

added theorem LinearEquiv.map_eq_zero_iff

added theorem LinearEquiv.map_ne_zero_iff

added theorem LinearEquiv.map_smul

added theorem LinearEquiv.mk_coe'

added theorem LinearEquiv.mk_coe

added def LinearEquiv.ofInvolutive

added def LinearEquiv.ofSubsingleton

added theorem LinearEquiv.ofSubsingleton_self

added def LinearEquiv.refl

added theorem LinearEquiv.refl_apply

added theorem LinearEquiv.refl_symm

added theorem LinearEquiv.refl_toLinearMap

added theorem LinearEquiv.refl_trans

added def LinearEquiv.restrictScalars

added theorem LinearEquiv.restrictScalars_inj

added theorem LinearEquiv.restrictScalars_injective

added theorem LinearEquiv.self_trans_symm

added def LinearEquiv.symm

added theorem LinearEquiv.symm_apply_apply

added theorem LinearEquiv.symm_apply_eq

added theorem LinearEquiv.symm_bijective

added theorem LinearEquiv.symm_comp_eq

added theorem LinearEquiv.symm_mk

added theorem LinearEquiv.symm_symm

added theorem LinearEquiv.symm_trans_apply

added theorem LinearEquiv.symm_trans_self

added theorem LinearEquiv.toAddEquiv_toIntLinearEquiv

added theorem LinearEquiv.toAddEquiv_toNatLinearEquiv

added theorem LinearEquiv.toAddMonoidHom_commutes

added def LinearEquiv.toEquiv

added theorem LinearEquiv.toEquiv_inj

added theorem LinearEquiv.toEquiv_injective

added theorem LinearEquiv.toFun_eq_coe

added theorem LinearEquiv.toLinearMap_inj

added theorem LinearEquiv.toLinearMap_injective

added theorem LinearEquiv.toLinearMap_symm_comp_eq

added def LinearEquiv.trans

added theorem LinearEquiv.trans_apply

added theorem LinearEquiv.trans_refl

added theorem LinearEquiv.trans_symm

added structure LinearEquiv

added def Module.compHom.toLinearEquiv

added def RingEquiv.toSemilinearEquiv