We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 543db0f commit f66a15cCopy full SHA for f66a15c
1 file changed
Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
@@ -497,6 +497,10 @@ section FastJacobi
497
We follow the implementation as in `Mathlib/Tactic/NormNum/LegendreSymbol.lean`.
498
-/
499
500
+-- `fastLegendreSym` is used for computing the Legendre symbol in a `norm_num` extension,
501
+-- i.e. needs to be used publicly.
502
+set_option backward.privateInPublic true
503
+
504
open NumberTheorySymbols jacobiSym
505
506
/-- Computes `J(a | b)` (or `-J(a | b)` if `flip` is set to `true`) given assumptions, by reducing
0 commit comments