Theorem jacobiSum_mem_algebraAdjoin_of_pow_eq_one

Modification history

2024-11-04 08:35
Mathlib/NumberTheory/JacobiSum/Basic.lean
chore: refactor roots of unity to avoid PNat (#18516) …
Modified jacobiSum_mem_algebraAdjoin_of_pow_eq_oneView 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 jacobiSum_mem_algebraAdjoin_of_pow_eq_oneView on Github →