Conflicting info on website about undergrad maths in mathlib

Stream: mathlib4

[Raghuram]

I just noticed that the list of undergraduate mathematics in and not in mathlib contradict each other in places (e.g., orthonormality of irreducible characters is listed as present yet it and even irreducible representation are listed as absent).

Would a PR removing the "missing" items which are obviously present (because they are on the "present" list and I check the link to see that it indeed exists) be welcome?

[Raghuram]

OK, this is more ambiguous than I thought:

• I'm not sure if "endomorphism exponential" and "matrix exponential" should be separate items.
• Ditto for "associative algebra" and "algebra" over a commutative ring (if the latter means a non-associative one, it's not that it can't be specifically defined so much as there is no reason to, for example, here it's just suggested to use a list of typeclass assumptions).
• "partial derivatives commute" is proven without defining directional or partial derivatives, by just applying the derivative (a linear map) to a vector. There isn't a definition to be linked to for directional or partial derivatives, but it does seem fair to say that (at least directional) derivatives are present.
• Similarly, there are series tests like the alternating series test with (not-necessarily unconditional) convergence of a series defined ad-hoc in the statement.

IG there is a common theme here of things that are basically in mathlib, but there isn't a single clean definition/theorem to point to. I'm not sure what to do about that.

[Eric Wieser]

Your first question is simple: things are listed as separate items iff the French curriculum this list was created from does the same

[Patrick Massot]

Raghuram said:

IG there is a common theme here of things that are basically in mathlib, but there isn't a single clean definition/theorem to point to. I'm not sure what to do about that.

Yes, this is the main difficulty with this list. Sometimes we add a somewhat vague declaration. You could also create a declaration specifically for this purpose. The danger is that people may want to start using it and complain there is no API for it, so we need a warning in the docstring.

[Patrick Massot]

It really depends on the item. For instance for commutativity of partial derivatives I think it’s fine to point to the abstract statement.