Theorem DirichletCharacter.primitiveCharacter_one

Modification history

2023-11-23 10:43
Mathlib/NumberTheory/DirichletCharacter/Basic.lean
feat: reduction of DirichletCharacter (#8440)
Added DirichletCharacter.primitiveCharacter_oneView on Github →