Zulip Chat Archive

Stream: general

Topic: nsmul_eq_mul


view this post on Zulip Sebastien Gouezel (Jun 07 2020 at 11:03):

The lemma nsmul_eq_mul states that

theorem nsmul_eq_mul [semiring R] (n : ) (a : R) : n  a = n * a :=
by rw [nsmul_eq_mul', nat.mul_cast_comm]

Since I never care about the weird integer multiplication (and I always take too long a time to find the name of this lemma), I would like to put a simp attribute on it, but maybe in other domains this would be a bad idea, so I thought I would ask here first. I uploaded a branch with the modification, and the linter complains about a lot of lemmas that are not any more in simp normal form (which should be expected), and about several simp lemmas that can now be proved automatically and therefore should not have the simp attribute any more. See https://github.com/leanprover-community/mathlib/runs/746885094

view this post on Zulip Johan Commelin (Jun 07 2020 at 14:16):

I guess it takes a lot of effort to fix this, but in principle I like it a a simp lemma

view this post on Zulip Mario Carneiro (Jun 07 2020 at 14:26):

I think this is fine as a simp lemma

view this post on Zulip Mario Carneiro (Jun 07 2020 at 14:27):

for semirings and up we pretty much always want to use multiplication in place of scalar multiple

view this post on Zulip Sebastien Gouezel (Jun 08 2020 at 07:42):

#2983


Last updated: May 10 2021 at 19:16 UTC