Def GradedMonoid.mkZeroMonoidHom

Modification history

2023-12-23 00:28

Mathlib/Algebra/GradedMonoid.lean

feat(Algebra/GradedMonoid): missing lemmas about `fst` and `snd` (#9227)

Modified GradedMonoid.mkZeroMonoidHom View on Github →

2023-01-27 17:01

Mathlib/Algebra/GradedMonoid.lean

feat: port Algebra.GradedMonoid (#1689)

Added GradedMonoid.mkZeroMonoidHom View on Github →