Commit 2023-11-15 16:58 eb292821

View on Github →

chore: redistribute some of the results in LinearAlgebra.Basic (#7801) This reduces the file from ~2600 lines to ~1600 lines.

Estimated changes

added theorem pi_eq_sum_univ
deleted theorem Submodule.coeSubtype
deleted theorem Submodule.coe_sum
added theorem Submodule.neg_coe
deleted theorem Submodule.subtype_apply
added theorem LinearMap.coeFn_sum
added theorem LinearMap.pow_restrict
added theorem LinearMap.sum_apply
added theorem Submodule.coeSubtype
added theorem Submodule.coe_ofLe
added theorem Submodule.coe_sum
added def Submodule.ofLe
added theorem Submodule.ofLe_apply
deleted theorem Finsupp.smul_sum
deleted def LinearMap.applyₗ'
deleted def LinearMap.applyₗ
deleted theorem LinearMap.coeFn_sum
deleted theorem LinearMap.coe_finsupp_sum
deleted theorem LinearMap.coe_smulRight
deleted def LinearMap.compRight
deleted theorem LinearMap.compRight_apply
deleted theorem LinearMap.pow_restrict
deleted def LinearMap.restrict
deleted theorem LinearMap.restrict_apply
deleted def LinearMap.smulRight
deleted theorem LinearMap.smulRight_apply
deleted theorem LinearMap.sum_apply
deleted theorem Submodule.coe_ofLe
deleted theorem Submodule.neg_coe
deleted def Submodule.ofLe
deleted theorem Submodule.ofLe_apply
deleted theorem Submodule.ofLe_injective
deleted theorem pi_eq_sum_univ
added theorem Finsupp.smul_sum