Commit 2024-04-05 15:59 3cc22ef5

chore: Sort big operator order lemmas (#11750) Take the content of

• some of Algebra.BigOperators.List.Basic
• some of Algebra.BigOperators.List.Lemmas
• some of Algebra.BigOperators.Multiset.Basic
• some of Algebra.BigOperators.Multiset.Lemmas
• Algebra.BigOperators.Multiset.Order
• Algebra.BigOperators.Order and sort it into six files:
• Algebra.Order.BigOperators.Group.List. I credit Yakov for https://github.com/leanprover-community/mathlib/pull/8543.
• Algebra.Order.BigOperators.Group.Multiset. Copyright inherited from Algebra.BigOperators.Multiset.Order.
• Algebra.Order.BigOperators.Group.Finset. Copyright inherited from Algebra.BigOperators.Order.
• Algebra.Order.BigOperators.Ring.List. I credit Stuart for https://github.com/leanprover-community/mathlib/pull/10184.
• Algebra.Order.BigOperators.Ring.Multiset. I credit Ruben for https://github.com/leanprover-community/mathlib/pull/8787.
• Algebra.Order.BigOperators.Ring.Finset. I credit Floris for https://github.com/leanprover-community/mathlib/pull/1294. Here are the design decisions at play:
• Pure algebra and big operators algebra shouldn't import (algebraic) order theory. This PR makes that better, but not perfect because we still import Data.Nat.Order.Basic in a few List files.
• It's Algebra.Order.BigOperators instead of Algebra.BigOperators.Order because algebraic order theory is more of a theory than big operators algebra. Another reason is that algebraic order theory is the only way to mix pure order and pure algebra, while there are more ways to mix pure finiteness and pure algebra than just big operators.
• There are separate files for group/monoid lemmas vs ring lemmas. Groups/monoids are the natural setup for big operators, so their lemmas shouldn't be mixed with ring lemmas that involves both addition and multiplication. As a result, everything under Algebra.Order.BigOperators.Group should be additivisable (except a few Nat- or Int-specific lemmas). In contrast, things under Algebra.Order.BigOperators.Ring are more prone to having heavy imports.
• Lemmas are separated according to List vs Multiset vs Finset. This is not strictly necessary, and can be relaxed in cases where there aren't that many lemmas to be had. As an example, I could split out the AbsoluteValue lemmas from Algebra.Order.BigOperators.Ring.Finset to a file Algebra.Order.BigOperators.Ring.AbsoluteValue and it could stay this way until too many lemmas are in this file (or a split is needed for import reasons), in which case we would need files Algebra.Order.BigOperators.Ring.AbsoluteValue.Finset, Algebra.Order.BigOperators.Ring.AbsoluteValue.Multiset, etc...
• Finsupp big operator and finprod/finsum order lemmas also belong in Algebra.Order.BigOperators. I haven't done so in this PR because the diff is big enough like that.