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) …

Added IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter View on Github →