Theorem IsPrimitiveRoot.autToPow_eq_ModularCyclotomicCharacter

Modification history

2025-05-02 14:44
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
chore(NumberTheory/Cyclotomic/CyclotomicCharacter): fix name to camelCase (#24521) …
Deleted IsPrimitiveRoot.autToPow_eq_ModularCyclotomicCharacterView on Github →
2024-11-04 08:35
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
chore: refactor roots of unity to avoid PNat (#18516) …
Modified IsPrimitiveRoot.autToPow_eq_ModularCyclotomicCharacterView on Github →
2024-03-18 09:20
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
feat: add mod n cyclotomic character (#6342) …
Added IsPrimitiveRoot.autToPow_eq_ModularCyclotomicCharacterView on Github →