Best place to report bugs/suggestions for Math in Lean?

Stream: general

[Martin C. Martin]

I've been reading Mathematics in Lean. Overall it's great, but every once in a while I find a typo. Where's the best place to report these? Somewhere in Zulip (where)? An issue in github? Something else?

[Patrick Massot]

An issue on GitHub is very good. A pull-request with a fix is even better.

[Martin C. Martin]

Done! https://github.com/avigad/mathematics_in_lean_source/pull/55

[Patrick Massot]

Thanks!

[Martin C. Martin]

You have a pair of pull requests here: https://github.com/avigad/mathematics_in_lean_source/pulls

One is from 2022 and has no comments, so I wonder if you missed it?

Also, in section 6.2 on algebraic structures, you have:

(mul_one: ∀ x : α, mul x one = x)
(one_mul: ∀ x : α, mul x one = x)

which, of course, are the same. I'm not sure the correct fix here: reverse the second one, or just get rid of it?

[Martin C. Martin]

Actually, I guess we'd eliminate the first one and fix the second one? Having both of them makes it closer to what's in mathlib, but as the end of section 2.2 points out, you can derive mul_one from one_mul along with mul_left_inv

[Martin C. Martin]

Also, a little later where we supply the additive definitions, neg should only take a single argument, whereas it currently takes a b : point.

[Martin C. Martin]

Also, our structure has a suffix of 1, so in add_group_point we need to add that suffix.

[Martin C. Martin]

In section 6.4, in the definition of norm for Euclidean domain, "N(a) < N(b)" should read "N(r) < N(b)."