Commit 2025-01-16 10:00 e9450cdc

View on Github →

refactor: make CanonicallyOrdered... mixin (#17444) This PR is the first step to migrate from semibundled ordered algebraic typeclasses to mixin typeclasses. This will significantly reduce the number of typeclasses and improve performance. See #20676. This PR introduces 2 typeclasses CanonicallyOrderedAdd CanonicallyOrderedMul and deprecates legacy semibundled CanonicallyOrdered* typeclasses.

Estimated changes

modified theorem geom_sum_lt
modified theorem geom_sum_of_lt_one
modified theorem geom_sum_of_one_lt
modified theorem geom₂_sum_of_gt
modified theorem geom₂_sum_of_lt
added theorem tsub_div
deleted theorem tsub_div
modified theorem NeZero.of_gt
modified theorem NeZero.pos
deleted theorem le_mul_left
deleted theorem le_mul_right
modified theorem le_self_mul
added theorem one_lt_of_gt
deleted theorem pos_of_gt
modified theorem Odd.pos
modified theorem mul_self_tsub_mul_self
modified theorem mul_tsub_one
modified theorem tsub_mul
modified theorem tsub_one_mul
modified theorem Nat.cast_finsetSup
modified theorem DFinsupp.single_le_iff
modified theorem Nat.cast_tsub
modified theorem IsFwInvariant.isInvariant
modified theorem measurableSet_eq_fun'
modified theorem hasProd_of_isLUB