Theorem ModularCyclotomicCharacter_aux_spec

Modification history

2025-04-06 18:39
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
feat(NumberTheory): p-adic cyclotomic character (#21934)
Deleted ModularCyclotomicCharacter_aux_specView on Github →
2024-11-04 08:35
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
chore: refactor roots of unity to avoid PNat (#18516) …
Modified ModularCyclotomicCharacter_aux_specView on Github →
2024-03-18 09:20
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
feat: add mod n cyclotomic character (#6342) …
Added ModularCyclotomicCharacter_aux_specView on Github →