Commit 2021-12-10 00:34 1ecdf714
View on Github →chore(algebra/punit_instances): add comm_cancel_monoid_with_zero, normalized_gcd_monoid, and scalar action instances (#10312)
Motivated by this Zulip thread.
This also moves the simp lemmas closer to the instances they refer to.