sub): split file (#16868)

Commit

3 years ago

chore(algebra/order/sub): split file (#16868) - [x] depends on: #16861 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author

kim-em

Parents

938f1f1b

mathlib 02b85de4 - chore(algebra/order/sub): split file (#16868)

mathlib
02b85de4 - chore(algebra/order/sub): split file (#16868)