Theorem ModularCyclotomicCharacter.toFun_spec''

Modification history

2024-03-18 09:20
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
feat: add mod n cyclotomic character (#6342) …
Added ModularCyclotomicCharacter.toFun_spec''View on Github →