Commit 2024-02-02 13:15 23d27aa1

View on Github →

chore(Algebra/Module/LinearMap): split into 3 files (#10183)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Equiv.lean

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

deleted def DistribMulAction.toLinearMap

deleted def DistribMulAction.toModuleEnd

deleted def LinearMap.applyₗ'

deleted def LinearMap.applyₗ

deleted theorem LinearMap.coe_mul

deleted theorem LinearMap.coe_one

deleted theorem LinearMap.coe_pow

deleted theorem LinearMap.coe_smulRight

deleted theorem LinearMap.commute_pow_left_of_commute

deleted def LinearMap.compRight

deleted theorem LinearMap.compRight_apply

deleted theorem LinearMap.id_pow

deleted theorem LinearMap.injective_of_iterate_injective

deleted theorem LinearMap.iterate_bijective

deleted theorem LinearMap.iterate_injective

deleted theorem LinearMap.iterate_succ

deleted theorem LinearMap.iterate_surjective

deleted theorem LinearMap.mul_apply

deleted theorem LinearMap.mul_eq_comp

deleted theorem LinearMap.one_apply

deleted theorem LinearMap.one_eq_id

deleted theorem LinearMap.pow_apply

deleted theorem LinearMap.pow_map_zero_of_le

deleted def LinearMap.smulRight

deleted theorem LinearMap.smulRight_apply

deleted theorem LinearMap.smulRight_apply_eq_zero_iff

deleted theorem LinearMap.smulRight_zero

deleted def LinearMap.smulRightₗ

deleted theorem LinearMap.smulRightₗ_apply

deleted theorem LinearMap.surjective_of_iterate_surjective

deleted theorem LinearMap.zero_smulRight

deleted theorem Module.End.intCast_apply

deleted theorem Module.End.intCast_def

deleted theorem Module.End.natCast_apply

deleted theorem Module.End.natCast_def

deleted theorem Module.End.ofNat_apply

deleted theorem Module.End_isUnit_apply_inv_apply_of_isUnit

deleted theorem Module.End_isUnit_inv_apply_apply_of_isUnit

deleted def Module.moduleEndSelf

deleted def Module.moduleEndSelfOp

deleted def Module.toModuleEnd

deleted theorem image_smul_set

deleted theorem image_smul_setₛₗ

deleted theorem preimage_smul_set

deleted theorem preimage_smul_setₛₗ

Created Mathlib/Algebra/Module/LinearMap/End.lean

added def DistribMulAction.toLinearMap

added def DistribMulAction.toModuleEnd

added def LinearMap.applyₗ'

added def LinearMap.applyₗ

added theorem LinearMap.coe_mul

added theorem LinearMap.coe_one

added theorem LinearMap.coe_pow

added theorem LinearMap.coe_smulRight

added theorem LinearMap.commute_pow_left_of_commute

added def LinearMap.compRight

added theorem LinearMap.compRight_apply

added theorem LinearMap.id_pow

added theorem LinearMap.injective_of_iterate_injective

added theorem LinearMap.iterate_bijective

added theorem LinearMap.iterate_injective

added theorem LinearMap.iterate_succ

added theorem LinearMap.iterate_surjective

added theorem LinearMap.mul_apply

added theorem LinearMap.mul_eq_comp

added theorem LinearMap.one_apply

added theorem LinearMap.one_eq_id

added theorem LinearMap.pow_apply

added theorem LinearMap.pow_map_zero_of_le

added def LinearMap.smulRight

added theorem LinearMap.smulRight_apply

added theorem LinearMap.smulRight_apply_eq_zero_iff

added theorem LinearMap.smulRight_zero

added def LinearMap.smulRightₗ

added theorem LinearMap.smulRightₗ_apply

added theorem LinearMap.surjective_of_iterate_surjective

added theorem LinearMap.zero_smulRight

added theorem Module.End.intCast_apply

added theorem Module.End.intCast_def

added theorem Module.End.natCast_apply

added theorem Module.End.natCast_def

added theorem Module.End.ofNat_apply

added theorem Module.End_isUnit_apply_inv_apply_of_isUnit

added theorem Module.End_isUnit_inv_apply_apply_of_isUnit

added def Module.moduleEndSelf

added def Module.moduleEndSelfOp

added def Module.toModuleEnd

Created Mathlib/Algebra/Module/LinearMap/Pointwise.lean

added theorem image_smul_set

added theorem image_smul_setₛₗ

added theorem preimage_smul_set

added theorem preimage_smul_setₛₗ

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

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean