Unscoping big operators

Stream: mathlib4

[Yaël Dillies]

Is it time that we unscope the notation for docs#Finset.sum, docs#Finset.prod ? It keeps being a point of confusion for beginners (although it effectively teaches them about open scoped) and in four years of existence nobody has come up with a conflicting notation.

[Martin Dvořák]

I prefer seeing Finset.sum in the Infoview.

[Miyahara Kō]

@Yaël Dillies #13181

[Miyahara Kō]

Oh no! There is a conflicting notations for CategoryTheory.Limits.piObj!

[Miyahara Kō]

It's inevitable but we change the notation of piObj from ∏ f to ∏ᶜ f.

[Martin Dvořák]

I'd like to take back my previous opinion.
Now that I work much more with sums and much less with Sigma types, the notation ∑ is lovely.
I cannot imagine writing the proof I just wrote without it...

  calc ∑ s, |∑ i, ∑ j, x i * y j * ((i ⬙ j) s - (j ⬙ i) s)|
     ≤ ∑ s, ∑ i, |∑ j, x i * y j * ((i ⬙ j) s - (j ⬙ i) s)| := ?_
   _ ≤ ∑ s, ∑ i, ∑ j, |x i * y j * ((i ⬙ j) s - (j ⬙ i) s)| := ?_
   _ = ∑ i, ∑ s, ∑ j, |x i * y j * ((i ⬙ j) s - (j ⬙ i) s)| := ?_
   _ = ∑ i, ∑ j, ∑ s, |x i * y j * ((i ⬙ j) s - (j ⬙ i) s)| := ?_
   _ = ∑ i, ∑ j, ∑ s, x i * y j * |((i ⬙ j) s - (j ⬙ i) s)| := ?_
   _ = ∑ i, ∑ j, x i * y j * ∑ s, |((i ⬙ j) s - (j ⬙ i) s)| := ?_
   _ = ∑ i, ∑ j, x i * y j * (2 * (i ⬙ j) 𝄩 (j ⬙ i)) := ?_
   _ ≤ ∑ i, ∑ j, x i * y j * (2 * ε) := ?_
   _ = ∑ i, ∑ j, 2 * ε * (x i * y j) := ?_
   _ = ∑ i, 2 * ε * ∑ j, (x i * y j) := ?_
   _ = 2 * ε * ∑ i, ∑ j, (x i * y j) := ?_
   _ = 2 * ε * 1 := ?_
   _ = 2 * ε := mul_one _

[Yuyang Zhao]

∑ is twice the width of Σ in the fonts I use, so I never worry about the confusion.

[Martin Dvořák]

I use monospace fonts, but there is still a visual difference — the summation symbol goes "deeper" into the line.