Commit 2023-01-27 17:01 d93927f9

View on Github →

feat: port Algebra.GradedMonoid (#1689)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GradedMonoid.lean

added def GradedMonoid.GMonoid.gnpowRec

added theorem GradedMonoid.GMonoid.gnpowRec_succ

added theorem GradedMonoid.GMonoid.gnpowRec_zero

added theorem GradedMonoid.GradeZero.smul_eq_mul

added theorem GradedMonoid.list_prod_map_eq_dProd

added theorem GradedMonoid.list_prod_ofFn_eq_dProd

added def GradedMonoid.mk

added def GradedMonoid.mkZeroMonoidHom

added theorem GradedMonoid.mk_list_dProd

added theorem GradedMonoid.mk_mul_mk

added theorem GradedMonoid.mk_pow

added theorem GradedMonoid.mk_zero_pow

added theorem GradedMonoid.mk_zero_smul

added def GradedMonoid

added def List.dProd

added def List.dProdIndex

added theorem List.dProdIndex_cons

added theorem List.dProdIndex_eq_map_sum

added theorem List.dProdIndex_nil

added theorem List.dProd_cons

added theorem List.dProd_monoid

added theorem List.dProd_nil

added def SetLike.Homogeneous

added theorem SetLike.coe_gMul

added theorem SetLike.coe_gOne

added theorem SetLike.coe_gnpow

added theorem SetLike.coe_list_dProd

added def SetLike.homogeneousSubmonoid

added theorem SetLike.homogeneous_coe

added theorem SetLike.homogeneous_mul

added theorem SetLike.homogeneous_one

added theorem SetLike.list_dProd_eq

added theorem SetLike.list_prod_map_mem_graded

added theorem SetLike.list_prod_ofFn_mem_graded

added theorem SetLike.mul_mem_graded

added theorem SetLike.one_mem_graded

added theorem SetLike.pow_mem_graded