Commit 2026-01-30 09:16 e8143064
View on Github →feat(DirichletCharacter): any element of the conductorSet is divisible by the conductor (#34569)
Prove the following result:
For χ a Dirichlet character and d ∈ χ.conductorSet, we have χ.conductor ∣ d