mathlib3

5306f2df - refactor(algebra/punit_instances): Move order instances (#15465)

refactor(algebra/punit_instances): Move order instances (#15465) The location of those instances means that order files need to pull out a bunch of algebra to use the (trivial) order structures on `punit`. This moves the `complete_boolean_algebra` instance to `order.complete_boolean_algebra` and splits off the `boolean_algebra` and `linear_order` instances. Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>