Theorem exists_jacobiSum_eq_neg_one_add

Modification history

2024-10-07 20:10
Mathlib/NumberTheory/JacobiSum/Basic.lean
chore(*): drop some `[Decidable*]` assumptions (#17396) …
Modified exists_jacobiSum_eq_neg_one_addView on Github →
2024-10-01 14:00
Mathlib/NumberTheory/JacobiSum/Basic.lean
feat(NumberTheory/JacobiSum/Basic): add lemmas on value of Jacobi sum (#17003) …
Added exists_jacobiSum_eq_neg_one_addView on Github →