mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore: split order synonym instances for GroupWithZero into their own file

Open Ruben-VandeVelde opened this issue 9 months ago • 3 comments

This is consistent with the Group file, and drops the dependency on Mathlib.Order entirely.

  • [x] depends on: #13008
  • [x] depends on: #13033

Open in Gitpod

Ruben-VandeVelde avatar May 17 '24 16:05 Ruben-VandeVelde