Theorem DirichletCharacter.factorsThrough_gcd

Modification history

2026-01-30 09:16
Mathlib/NumberTheory/DirichletCharacter/Basic.lean
feat(DirichletCharacter): any element of the `conductorSet` is divisible by the conductor (#34569) …
Added DirichletCharacter.factorsThrough_gcdView on Github →