Theorem ModularCyclotomicCharacter.unique

Modification history

2024-08-30 08:52
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
style: some formatting fixes (#16263) …
Modified ModularCyclotomicCharacter.uniqueView on Github →
2024-03-18 09:20
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
feat: add mod n cyclotomic character (#6342) …
Added ModularCyclotomicCharacter.uniqueView on Github →