Commit 2023-10-05 06:34 f3bc24c3

View on Github →

chore: rename CanonicallyOrderedAddMonoid to ..AddCommMonoid (#7503) Renames: CanonicallyOrderedMonoid -> CanonicallyOrderedCommMonoid CanonicallyOrderedAddMonoid -> CanonicallyOrderedAddCommMonoid CanonicallyLinearOrderedMonoid -> CanonicallyLinearOrderedCommMonoid CanonicallyLinearOrderedAddMonoid -> CanonicallyLinearOrderedAddCommMonoid

Estimated changes

modified theorem Finset.sum_range_tsub
modified theorem Multiset.le_prod_of_mem
modified theorem Multiset.prod_eq_one_iff
modified theorem NeZero.of_gt
modified theorem NeZero.pos
modified theorem pos_of_gt
modified theorem Even.tsub
modified theorem List.monotone_prod_take
modified theorem List.prod_eq_one_iff
modified theorem IsFwInvariant.isInvariant
modified theorem hasSum_of_isLUB