Commit 2024-12-21 08:53 14683753

View on Github →

refactor: rename lemmas about IsReduced to work with dot notation (#20135) We rename some lemmas about reduced words in Coxeter groups so that they can be used with dot notation.

  • CoxeterSystem.isReduced_reverse is renamed to CoxeterSystem.isReduced_reverse_iff, and its forward direction is given the new name CoxeterSystem.IsReduced.reverse.
  • CoxeterSystem.isReduced_take is renamed to CoxeterSystem.IsReduced.take.
  • CoxeterSystem.isReduced_drop is renamed to CoxeterSystem.IsReduced.drop. To be completely honest, I'm on the fence about this one, but I'd like to see what others think.

Estimated changes