Commit 2023-02-02 11:28 de1a0155

View on Github →

feat: port Algebra.GradedMulAction (#1959)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GradedMonoid.lean

Created Mathlib/Algebra/GradedMulAction.lean

added theorem GradedMonoid.mk_smul_mk

added theorem SetLike.Homogeneous.graded_smul

added theorem SetLike.coe_GSmul