mathlib

dc1525fb - docs(data/sum/basic): Expand module docstring and cleanup (#11158)

docs(data/sum/basic): Expand module docstring and cleanup (#11158) This moves `data.sum` to `data.sum.basic`, provides a proper docstring for it, cleans it up. There are no new declarations, just some file rearrangement, variable grouping, unindentation, and a `protected` attribute for `sum.lex.inl`/`sum.lex.inr` to avoid them clashing with `sum.inl`/`sum.inr`.