Skip to content

Commit

Permalink
doc(algebra/big_operators): fix formatting of library note (#6261)
Browse files Browse the repository at this point in the history
  • Loading branch information
robertylewis committed Feb 16, 2021
1 parent 362619e commit 2411d68
Showing 1 changed file with 0 additions and 2 deletions.
2 changes: 0 additions & 2 deletions src/algebra/big_operators/basic.lean
Expand Up @@ -49,8 +49,6 @@ rfl
end finset

/--
## Operator precedence of `∏` and `∑`
There is no established mathematical convention
for the operator precedence of big operators like `∏` and `∑`.
We will have to make a choice.
Expand Down

0 comments on commit 2411d68

Please sign in to comment.