Theorem MulChar.exists_apply_sub_one_mul_apply_sub_one

Modification history

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_mul_apply_sub_oneView on Github →