Theorem MulChar.exists_apply_sub_one_eq_mul_sub_one

Modification history

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