Commit 2025-04-09 03:14 13df8d6d

View on Github →

chore: split Algebra.Order.GroupWithZero.Unbundled (#23828)

  • .Defs contains the definitions of the eight typeclasses and everything that does not require MulZeroClass/MulOneClass.
  • .Basic contains everything else.

Estimated changes

deleted theorem le_of_mul_le_mul_left
deleted theorem le_of_mul_le_mul_right
deleted theorem lt_of_mul_lt_mul_left
deleted theorem lt_of_mul_lt_mul_right
deleted theorem mul_le_mul_left
deleted theorem mul_le_mul_of_nonneg'
deleted theorem mul_le_mul_of_nonneg
deleted theorem mul_le_mul_of_nonneg_left
deleted theorem mul_le_mul_right
deleted theorem mul_lt_mul_left
deleted theorem mul_lt_mul_of_pos'
deleted theorem mul_lt_mul_of_pos
deleted theorem mul_lt_mul_of_pos_left
deleted theorem mul_lt_mul_of_pos_right
deleted theorem mul_lt_mul_right
deleted theorem posMulMono_iff_mulPosMono
added theorem le_of_mul_le_mul_left
added theorem le_of_mul_le_mul_right
added theorem lt_of_mul_lt_mul_left
added theorem lt_of_mul_lt_mul_right
added theorem mul_le_mul_left
added theorem mul_le_mul_of_nonneg'
added theorem mul_le_mul_of_nonneg
added theorem mul_le_mul_right
added theorem mul_lt_mul_left
added theorem mul_lt_mul_of_pos'
added theorem mul_lt_mul_of_pos
added theorem mul_lt_mul_of_pos_left
added theorem mul_lt_mul_right