interval): Interval arithmetic (#16761)

Commit

3 years ago

feat(algebra/order/interval): Interval arithmetic (#16761) Define arithmetic operations on `interval`/`nonempty_interval` and prove their correctness.

Author

YaelDillies

Parents

7ac96dea

mathlib3 1a513788 - feat(algebra/order/interval): Interval arithmetic (#16761)

mathlib3
1a513788 - feat(algebra/order/interval): Interval arithmetic (#16761)