mathlib3
1ecdf714 - chore(algebra/punit_instances): add `comm_cancel_monoid_with_zero`, `normalized_gcd_monoid`, and scalar action instances (#10312)

Commit
4 years ago
chore(algebra/punit_instances): add `comm_cancel_monoid_with_zero`, `normalized_gcd_monoid`, and scalar action instances (#10312) Motivated by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Is.200.20not.20equal.20to.201.3F/near/261366868). This also moves the simp lemmas closer to the instances they refer to. Co-authored-by: Anne Baanen <vierkantor@vierkantor.com>
Author
Parents
Loading