add_monoid N

Stream: new members

[Bhavik Mehta]

I've got add_monoid.smul now (from sum_const in algebra/big_operators.lean) in the case of the monoid ℕ, and I can't find a lemma for

example {a b : ℕ} : add_monoid.smul a b = a * b

It's probably not hard by induction, but I can't see any shorter way - where it feels like there should be
Edit: I wasn't looking hard enough, it's nat.smul_eq_mul

[Kevin Buzzard]

Did you try library_search?

[Simon Hudon]

@Bhavik Mehta I don't think you need to strike out your own comment. Just add your final remark as a new message. Other people can still learn from your question even if you find it silly in hindsight.

[Bhavik Mehta]

I was tempted to delete it entirely! But yes, this is the precise reason it's still readable :)