C01_Introduction.html

Stream: new members

[some.knowit]

Hi, I am a complete newbie, reading

https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html

I have many questions, so I'd start with the first :) I see:

we did with the phrase by rw [hk, mul_left_comm] in the example above.

But here is no mul_left_comm on that page. Is that a typo?

[some.knowit]

I've just opened a pull request on this. Can some maintainer of the repo please take a look? (Apparently the Github workflow needs approval to run.)

[some.knowit]

btw, I've been following and playing with the math in lean tutorial. So far super fun!