Zulip Chat Archive

Stream: general

Topic: nsmul


view this post on Zulip Kenny Lau (May 31 2020 at 07:46):

PSA:

rss-bot said:

chore(algebra/group_hom): rename add_monoid.smul to nsmul (#2861)
chore(algebra/group_hom): rename add_monoid.smul to nsmul (#2861)

Also drop as a notation for two smuls declared in this file,
use •ℕ and •ℤ instead.

This way one can immediately see that a lemma uses nsmul/gsmul, not has_scalar.smul.
https://github.com/leanprover-community/mathlib/commit/a285049b81c622ccea3d292a09ec979bcf7a1547

view this post on Zulip Yury G. Kudryashov (May 31 2020 at 07:57):

What means "PSA"?

view this post on Zulip Kenny Lau (May 31 2020 at 07:58):

Public Service Announcement


Last updated: May 08 2021 at 19:11 UTC