Theorem modularCyclotomicCharacter.toFun_unique'

Modification history

2026-07-01 13:18
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
chore(NumberTheory/NumberField/Units/Basic): use `Nat.card` instead of `Fintype.card` (#41210) …
Modified modularCyclotomicCharacter.toFun_unique'View on Github →
2025-05-02 14:44
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
chore(NumberTheory/Cyclotomic/CyclotomicCharacter): fix name to camelCase (#24521) …
Added modularCyclotomicCharacter.toFun_unique'View on Github →