mathlib3

07f9b8e1 - feat(data/sum/order): Linear and disjoint sums of orders (#11157)

feat(data/sum/order): Linear and disjoint sums of orders (#11157) This defines the disjoint sum of two orders on `α ⊕ β` and the linear (aka lexicographic) sum of two orders on `α ⊕ₗ β` (a type synonym of `α ⊕ β`) in a new file `data.sum.order`.