mathlib

14c52e99 - feat(data/set/intervals/instances): algebraic instances for unit intervals (#15712)

feat(data/set/intervals/instances): algebraic instances for unit intervals (#15712) Proving `cancel_comm_monoid_with_zero (Icc 0 1)`, `comm_semigroup (Ico 0 1)`, `comm_monoid (Ioc 0 1)`, and `comm_semigroup (Ioo 0 1)` for suitably structured underlying type `α`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>