Zulip Chat Archive

Stream: general

Topic: nsmul

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

Yury G. Kudryashov (May 31 2020 at 07:57):

What means "PSA"?

Kenny Lau (May 31 2020 at 07:58):

Public Service Announcement

Last updated: Dec 20 2023 at 11:08 UTC