Theorem DirichletCharacter.changeLevel_primitiveCharacter

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.changeLevel_primitiveCharacterView on Github →