Commit 2022-12-21 05:43 489f1045

View on Github →

feat: port Algebra.SmulWithZero (#1130)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/SmulWithZero.lean

added def MulActionWithZero.compHom

added def SmulWithZero.compHom

added def smulMonoidWithZeroHom

added theorem smul_inv₀

added theorem zero_smul