open_locale big_operators

Stream: mathlib4

[Xavier Roblot]

I am working on RingTheory.Prime. The mathlib3 file starts with open_locale big_operators that mathport translates into open BigOperators which gives an error. But, in fact, deleting this line does not cause any error and the big operators notations appear to work just fine.

Is deleting this line indeed the correct fix here?

[Ruben Van de Velde]

Hm, I thought @Johan Commelin had got the locale thing to work

[Johan Commelin]

At the moment, the notation is global

[Johan Commelin]

@Xavier Roblot Please leave a porting note

[Xavier Roblot]

Ok. I will do that. Thanks.

[Shreyas Srinivas]

I encountered the same thing in Data.Nat.Fib. Mathlib port had translated it to open BigOperators