Commit 2024-10-01 14:00 608231ac
View on Github →feat(NumberTheory/JacobiSum/Basic): add lemmas on value of Jacobi sum (#17003)
This adds statements that the Jacobi sum of two characters of order dividing n is in ℤ[μ], where μ is a primitive nth root of unity, and more precisely, is of the form -1 + z*(μ-1)^2 with z in ℤ[μ].