Skip to content

Commit

Permalink
doc(number_theory/legendre_symbol/jacobi_symbol): remove now spurious…
Browse files Browse the repository at this point in the history
… reference to 'subscript J' (#16541)

This PR just fixes the docstring for the notation. The reference to "no subscript J in unicode" doesn't make sense anymore after the notation was changed to `J(a | b)`.
  • Loading branch information
MichaelStollBayreuth committed Sep 18, 2022
1 parent 1dc531a commit 7e74869
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/number_theory/legendre_symbol/jacobi_symbol.lean
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ Jacobi symbol when `b` is odd and gives less meaningful values when it is not (e
is `1` when `b = 0`). This is called `jacobi_sym a b`.
We define localized notation (locale `number_theory_symbols`) `J(a | b)` for the Jacobi
symbol `jacobi_sym a b`. (Unfortunately, there is no subscript "J" in unicode.)
symbol `jacobi_sym a b`.
-/

open nat zmod
Expand Down

0 comments on commit 7e74869

Please sign in to comment.