subdirs

Stream: general

[Yury G. Kudryashov]

Hi, do we have a description of the directory structure? In particular, where is the line between algebra/group* and group_theory/*?

[Kevin Buzzard]

They grew organically. I suspect people might be open to suggested rearrangements

[Kevin Buzzard]

Things are certainly occasionally rearranged

[Floris van Doorn]

Most things in algebra/group/ are lemmas about equational reasoning between elements in a group.
Everything else is in group_theory/, like subgroups, quotient groups and anything more advanced.

I don't know the libraries that well, so this is probably not completely right, but it is a good heuristic.

[Scott Morrison]

I feel like this distinction is also pretty close to the dividing line between when it makes sense to unbundle and use typeclasses (equational reasoning about elements), and when it makes sense to bundle (and use category theory...) (when you're interesting in relationships between the containers).