simp smul_add

Stream: new members

[Nicolò Cavalleri]

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]

mul_add isn't tagged simp either.

[Nicolò Cavalleri]

Then I wonder why mul_add is also not simp... is there a tactic like ring that works for calculations in modules?

[Notification Bot]

This topic was moved by Scott Morrison to #general > simp smul_add