to_interval_mod): notation for `add_comm_group.modeq` (#18955)

Commit

3 years ago

feat(algebra/order/to_interval_mod): notation for `add_comm_group.modeq` (#18955) Split from #18941

Author

eric-wieser

Parents