Commit 2023-05-18 15:44 b9104ba6

View on Github →

feat port: Algebra.DirectSum.Internal (#4078)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/DirectSum/Internal.lean

added def DirectSum.coeAlgHom

added theorem DirectSum.coeAlgHom_of

added def DirectSum.coeRingHom

added theorem DirectSum.coeRingHom_of

added theorem DirectSum.coe_mul_apply

added theorem DirectSum.coe_mul_apply_eq_dfinsupp_sum

added theorem DirectSum.coe_mul_of_apply

added theorem DirectSum.coe_mul_of_apply_add

added theorem DirectSum.coe_mul_of_apply_aux

added theorem DirectSum.coe_mul_of_apply_of_le

added theorem DirectSum.coe_mul_of_apply_of_not_le

added theorem DirectSum.coe_of_mul_apply

added theorem DirectSum.coe_of_mul_apply_add

added theorem DirectSum.coe_of_mul_apply_aux

added theorem DirectSum.coe_of_mul_apply_of_le

added theorem DirectSum.coe_of_mul_apply_of_not_le

added theorem SetLike.Homogeneous.smul

added theorem SetLike.algebraMap_mem_graded

added theorem SetLike.homogeneous_zero_submodule

added theorem SetLike.int_cast_mem_graded

added theorem SetLike.nat_cast_mem_graded

added theorem Submodule.iSup_eq_toSubmodule_range

added theorem Submodule.setLike.coe_galgebra_toFun