Documenting recommended imports

Stream: mathlib4

[Artie Khovanov]

Even elements are defined in Algebra.Group.Even. However, due to wanting to optimise the import graph, all lemmas about even elements that mention a 1 or multiplication are in Algebra.Ring.Parity. This means that the simp automation only works properly if Algebra.Ring.Parity is imported, which is not obvious to a user who is looking up where lemmas about even elements are ("why can't I prove 0 is a square? why can't I prove 2 is even?").

How can I communicate to users of Algebra.Group.Even that they may also want to import Algebra.Ring.Parity? I've added a note in the documentation header but there might be a better way?

#20558

[Ruben Van de Velde]

A reference in the module documentation probably makes most sense, yeah

[Damiano Testa]

More generally, I find that Even/IsSquare are very good and useful concepts.

[Damiano Testa]

Odd, however, always strikes me as much less well-defined.

[Damiano Testa]

For instance, I am not even sure that the "correct" definition of Odd is what mathlib has, or whether it should simply be the negation of Even.

[Damiano Testa]

The fact that it does not even have an attempt at a multiplicative version does not improve the situation.

[Damiano Testa]

It is a little sad that the Even lemmas suffer because of the Odd situation. :smile:

[Artie Khovanov]

Damiano Testa said:

It is a little sad that the Even lemmas suffer because of the Odd situation. :smile:

I don't think this is why. The reason some "simple" simp lemmas about even elements / squares are in the Ring.Parity file is that the Group.Even file is not allowed to know about a Ring or even a GroupWithZero.

[Artie Khovanov]

Damiano Testa said:

For instance, I am not even sure that the "correct" definition of Odd is what mathlib has, or whether it should simply be the negation of Even.

The fact that you have to keep using two_mul to convert between (the definitions of) Odd and Even seems.. not ideal.