Commit 2023-03-17 16:27 a781fc87

View on Github →

feat: port Algebra.DirectSum.Module (#2596)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/DirectSum/Module.lean

added theorem DirectSum.IsInternal.addSubgroup_independent

added theorem DirectSum.IsInternal.addSubmonoid_independent

added theorem DirectSum.IsInternal.collectedBasis_coe

added theorem DirectSum.IsInternal.collectedBasis_mem

added theorem DirectSum.IsInternal.isCompl

added theorem DirectSum.IsInternal.submodule_independent

added theorem DirectSum.IsInternal.submodule_supᵢ_eq_top

added theorem DirectSum.apply_eq_component

added def DirectSum.coeLinearMap

added theorem DirectSum.coeLinearMap_of

added theorem DirectSum.coe_toModule_eq_coe_toAddMonoid

added theorem DirectSum.component.lof_self

added theorem DirectSum.component.of

added def DirectSum.component

added theorem DirectSum.ext

added theorem DirectSum.ext_iff

added theorem DirectSum.isInternal_submodule_iff_independent_and_supᵢ_eq_top

added theorem DirectSum.isInternal_submodule_iff_isCompl

added theorem DirectSum.isInternal_submodule_of_independent_of_supᵢ_eq_top

added def DirectSum.lequivCongrLeft

added theorem DirectSum.lequivCongrLeft_apply

added def DirectSum.linearEquivFunOnFintype

added theorem DirectSum.linearEquivFunOnFintype_lof

added theorem DirectSum.linearEquivFunOnFintype_symm_coe

added theorem DirectSum.linearEquivFunOnFintype_symm_single

added theorem DirectSum.linearMap_ext

added def DirectSum.lmk

added def DirectSum.lof

added theorem DirectSum.lof_apply

added theorem DirectSum.lof_eq_of

added def DirectSum.lsetToSet

added theorem DirectSum.mk_smul

added theorem DirectSum.of_smul

added theorem DirectSum.sigmaLcurry_apply

added theorem DirectSum.sigmaLuncurry_apply

added theorem DirectSum.single_eq_lof

added theorem DirectSum.smul_apply

added theorem DirectSum.support_smul

added theorem DirectSum.toModule.unique

added def DirectSum.toModule

added theorem DirectSum.toModule_lof

Modified Mathlib/Data/Dfinsupp/Basic.lean