mathlib
b4201e7b - chore(group/ring_hom): fix a nat nsmul diamond (#7201)

Commit
4 years ago
chore(group/ring_hom): fix a nat nsmul diamond (#7201) The space of additive monoid should be given a proper `nat`-action, by the pointwise action, to avoid diamonds. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading