Commit 2024-03-28 11:53 bb349f30

View on Github →

chore: Reduce scope of LinearOrderedCommGroupWithZero (#11716) Reconstitute the file Algebra.Order.Monoid.WithZero from three files:

  • Algebra.Order.Monoid.WithZero.Defs
  • Algebra.Order.Monoid.WithZero.Basic
  • Algebra.Order.WithZero Avoid importing it in many files. Most uses were just to get le_zero_iff to work on Nat. Before pre_11716 After post_11716

Estimated changes

modified theorem kstar_zero
added theorem WithZero.coe_le_coe
added theorem WithZero.coe_lt_coe
added theorem WithZero.zero_eq_bot
added theorem WithZero.zero_le
added theorem WithZero.zero_lt_coe
modified theorem inv_mul_lt_of_lt_mul₀
modified theorem mul_inv_lt_of_lt_mul₀
modified theorem zero_le'
deleted theorem WithZero.coe_le_coe
deleted theorem WithZero.coe_lt_coe
deleted theorem WithZero.zero_eq_bot
deleted theorem WithZero.zero_le
deleted theorem WithZero.zero_lt_coe