Stream: new members

Bhavik Mehta (Nov 20 2019 at 22:22):

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 (Nov 20 2019 at 22:35):

Did you try library_search?

Simon Hudon (Nov 21 2019 at 14:24):

@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 (Nov 21 2019 at 14:25):

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

Last updated: May 13 2021 at 23:16 UTC