Stream: new members
Topic: simp smul_add
Nicolò Cavalleri (Aug 03 2020 at 17:40):
Why is not
smul_add marked simp? I alway find myself writing
squeeze_simp and then having to add it manually! It looks like the typical kind of lemma that helps creating a normal form and hence should be marked simp...
Kevin Buzzard (Aug 03 2020 at 18:19):
mul_add isn't tagged
Nicolò Cavalleri (Aug 03 2020 at 19:13):
Then I wonder why
mul_add is also not simp... is there a tactic like
ring that works for calculations in modules?
Notification Bot (Aug 03 2020 at 22:53):
This topic was moved by Scott Morrison to #general > simp smul_add
Last updated: May 10 2021 at 17:39 UTC