Commit 2023-11-23 10:43 0cacf073

View on Github →

feat: reduction of DirichletCharacter (#8440)

Estimated changes

Modified Mathlib/Data/ZMod/Units.lean

modified theorem ZMod.IsUnit_cast_of_dvd

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean

added theorem DirichletCharacter.conductor_le_conductor_mem_conductorSet

added theorem DirichletCharacter.primitiveCharacter_isPrimitive

added theorem DirichletCharacter.primitiveCharacter_one