Zulip Chat Archive

Stream: new members

Topic: simp smul_add


view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 18:19):

mul_add isn't tagged simp either.

view this post on Zulip 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?

view this post on Zulip 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