mathlib
4c2bfdeb - chore(order/pilex): add docstring (#7769)

Commit

4 years ago

chore(order/pilex): add docstring (#7769) - add module docstring - extend `ordered_add_comm_group (pilex ι β)` using `to_additive`

Author

YaelDillies

Parents