mathlib3

96c1d69b - doc(data/list/*): Elaborate module docstrings (#9076)

doc(data/list/*): Elaborate module docstrings (#9076) Just adding some elaboration that @YaelDillies requested in #8867, but which didn't get included before it was merged.