Commit 2024-11-05 09:15 97dc6e83
View on Github →chore(Algebra/BigOperators): don't import Sym in the definition of big operators (#18650)
In the spirit of late imports, I came across this lemma that wants us to import Mathlib.Data.Finset.Sym and Mathlib.Data.Sym.Sym2.Order right at the end of the definition of big operators.