Commit 2024-07-19 02:45 3fef63ff

View on Github →

chore: split Algebra/Module/Equiv (#14466)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Lie/Basic.lean

Renamed Mathlib/Algebra/Module/Equiv.lean to Mathlib/Algebra/Module/Equiv/Basic.lean

deleted def LinearEquiv.Simps.apply

deleted def LinearEquiv.Simps.symm_apply

deleted theorem LinearEquiv.apply_symm_apply

deleted theorem LinearEquiv.coe_coe

deleted theorem LinearEquiv.coe_injective

deleted theorem LinearEquiv.coe_mk

deleted theorem LinearEquiv.coe_ofInvolutive

deleted theorem LinearEquiv.coe_symm_mk

deleted theorem LinearEquiv.coe_toAddEquiv

deleted theorem LinearEquiv.coe_toEquiv

deleted theorem LinearEquiv.coe_toEquiv_symm

deleted theorem LinearEquiv.coe_toLinearMap

deleted theorem LinearEquiv.coe_trans

deleted theorem LinearEquiv.comp_coe

deleted theorem LinearEquiv.comp_symm_eq

deleted theorem LinearEquiv.comp_toLinearMap_symm_eq

deleted theorem LinearEquiv.eq_comp_symm

deleted theorem LinearEquiv.eq_comp_toLinearMap_symm

deleted theorem LinearEquiv.eq_symm_apply

deleted theorem LinearEquiv.eq_symm_comp

deleted theorem LinearEquiv.eq_toLinearMap_symm_comp

deleted theorem LinearEquiv.ext

deleted theorem LinearEquiv.ext_iff

deleted theorem LinearEquiv.invFun_eq_symm

deleted theorem LinearEquiv.map_eq_zero_iff

deleted theorem LinearEquiv.map_ne_zero_iff

deleted theorem LinearEquiv.map_smul

deleted theorem LinearEquiv.mk_coe'

deleted theorem LinearEquiv.mk_coe

deleted def LinearEquiv.ofInvolutive

deleted def LinearEquiv.refl

deleted theorem LinearEquiv.refl_apply

deleted theorem LinearEquiv.refl_symm

deleted theorem LinearEquiv.refl_toLinearMap

deleted theorem LinearEquiv.refl_trans

deleted theorem LinearEquiv.self_trans_symm

deleted def LinearEquiv.symm

deleted theorem LinearEquiv.symm_apply_apply

deleted theorem LinearEquiv.symm_apply_eq

deleted theorem LinearEquiv.symm_bijective

deleted theorem LinearEquiv.symm_comp_eq

deleted theorem LinearEquiv.symm_mk

deleted theorem LinearEquiv.symm_symm

deleted theorem LinearEquiv.symm_trans_apply

deleted theorem LinearEquiv.symm_trans_self

deleted theorem LinearEquiv.toAddMonoidHom_commutes

deleted def LinearEquiv.toEquiv

deleted theorem LinearEquiv.toEquiv_inj

deleted theorem LinearEquiv.toEquiv_injective

deleted theorem LinearEquiv.toFun_eq_coe

deleted theorem LinearEquiv.toLinearMap_inj

deleted theorem LinearEquiv.toLinearMap_injective

deleted theorem LinearEquiv.toLinearMap_symm_comp_eq

deleted def LinearEquiv.trans

deleted theorem LinearEquiv.trans_apply

deleted theorem LinearEquiv.trans_refl

deleted theorem LinearEquiv.trans_symm

deleted structure LinearEquiv

deleted def RingEquiv.toSemilinearEquiv

deleted def SemilinearEquivClass.semilinearEquiv

Created Mathlib/Algebra/Module/Equiv/Defs.lean

added def LinearEquiv.Simps.apply

added def LinearEquiv.Simps.symm_apply

added theorem LinearEquiv.apply_symm_apply

added theorem LinearEquiv.coe_coe

added theorem LinearEquiv.coe_injective

added theorem LinearEquiv.coe_mk

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.refl

added theorem LinearEquiv.refl_apply

added theorem LinearEquiv.refl_symm

added theorem LinearEquiv.refl_toLinearMap

added theorem LinearEquiv.refl_trans

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.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 RingEquiv.toSemilinearEquiv

added def SemilinearEquivClass.semilinearEquiv

Modified Mathlib/Algebra/Module/LinearMap/Star.lean

Modified Mathlib/Algebra/Module/Opposites.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

Modified Mathlib/Algebra/Module/ULift.lean

Modified Mathlib/Algebra/Star/Module.lean

Modified Mathlib/CategoryTheory/Linear/Basic.lean

Modified Mathlib/Data/Finsupp/ToDFinsupp.lean

Modified Mathlib/LinearAlgebra/FiniteSpan.lean

Modified Mathlib/LinearAlgebra/GeneralLinearGroup.lean

Modified Mathlib/LinearAlgebra/Pi.lean

Modified Mathlib/LinearAlgebra/Quotient.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

Modified Mathlib/Topology/Algebra/UniformConvergence.lean

Modified scripts/noshake.json