New chapter in MIL

Stream: general

[Patrick Massot]

There is a new chapter in Mathematics in Lean. As usual we are interested in any corrections you could have, or any information about what is difficult to understand.

[Jireh Loreaux]

for typos and things like that, would you prefer a list or a PR?

[Patrick Massot]

A PR is better of course. The relevant repo is https://github.com/avigad/mathematics_in_lean_source

[Jireh Loreaux]

https://github.com/avigad/mathematics_in_lean_source/pull/142 for the PR about typos and style. It should be an easy review. Overall, this chapter flowed really well; I think it's great!

Two things I noticed while reading:

1. Early on when discussing morphisms, the proofs used f.map_mul or f.map_inv as opposed to map_mul f and map_inv f. Of course this is minor, but at the same time, it doesn't seem like these kinds of generic hom-class lemmas were discussed in the previous chapter (7.2: Hierarchies - Morphisms), so maybe the point to do it is here?
2. Upon introducing the polynomial notation R[X], I think that special emphasis should be placed on the fact that this is only syntax, the X has no meaning. It's not like R[Y] gives you polynomials in a different indeterminate. The same goes for Polynomial.X which gets abbreviated to X in the examples. On a cursory read, I can imagine a newcomer (especially students) being confused about the fact that Y doesn't work if you replace X everywhere.

[Patrick Massot]

Thank you very much for your patience correcting all those white space issues in particular. Your remarks are also useful. I don't have time to work on them now but I'll open an issue.

[Eric Wieser]

As a slight aside, my takeaway from

More generally, given an ring morphism f : R →+* S one can evaluate P : R[X] at a point
in S using Polynomial.eval₂. This one produces an actual function from R[X] to S
since it does not assume the existence of a Algebra R S instance, so dot notation works as
you would expect.

#check (Complex.ofReal : ℝ →+* ℂ)

is that we should remove docs#Complex.ofReal because it's just algebraMap!

[Jireh Loreaux]

Isn't the point that we need some def to apply the @[coe] attribute to though?

[Eric Wieser]

That's docs#Complex.ofReal'