Zulip Chat Archive

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 simp either.

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: Dec 20 2023 at 11:08 UTC