mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: partial port of Algebra/Order/

Open kim-em opened this issue 3 years ago • 1 comments
trafficstars

These aren't complete ports, mostly just the typeclass definition parts of

  • Algebra.Order.Monoid
  • Algebra.Order.Group
  • Algebra.Order.Ring

Creating these typeclasses with sorried instances for use with linarith was barely easier than porting the instances too.

  • [x] depends on #467

kim-em avatar Oct 14 '22 02:10 kim-em

The linter is failing because of https://github.com/leanprover/lean4/issues/1730.

kim-em avatar Oct 14 '22 10:10 kim-em

bors merge

kim-em avatar Oct 23 '22 22:10 kim-em

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 23 '22 22:10 bors[bot]