Commit 2022-10-23 22:19 a26dc822

View on Github →

feat: partial port of Algebra/Order/ (#470) 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.

Estimated changes

added theorem Left.one_lt_inv_iff
added theorem one_lt_div'
added theorem le_of_mul_le_mul_left'
added theorem lt_of_mul_lt_mul_left'
added theorem mul_le_mul_iff_left
added theorem mul_le_mul_iff_right
added theorem mul_le_mul_left'
added theorem mul_lt_mul_iff_left
added theorem mul_lt_mul_iff_right
added theorem mul_lt_mul_left'