binding prod / vs sum -

Stream: general

[Bolton Bailey]

Noticed something interesting when converting a lemma to a to_additive form. In the expression
∑ k in range m, f k - ∑ k in range n, f k
The ∑s bind tighter and the expression is interpreted correctly. But when I convert this to
∏ k in range m, f k / ∏ k in range n, f k
The first ∏ binds the whole expression. Is this intended?

[Yaël Dillies]

Yes, have a look at the module docstring of file#algebra/big_operators/basic

[Anne Baanen]

Yaël Dillies said:

Yes, have a look at the module docstring of file#algebra/big_operators/basic

I don't see anything about the precedence in the module docs...

[Anne Baanen]

Aha, it's a bit lower

[Kevin Buzzard]

It's this, not the actual module doc