Commit 2023-09-24 12:02 e6937e6c

View on Github →

feat: conductor of Dirichlet character (#7320)

Estimated changes

Modified Mathlib/Data/ZMod/Units.lean

added theorem ZMod.IsUnit_cast_of_dvd

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean

added theorem DirichletCharacter.FactorsThrough.dvd

added theorem DirichletCharacter.FactorsThrough.eq_changeLevel

added theorem DirichletCharacter.FactorsThrough.same_level

added def DirichletCharacter.FactorsThrough.χ₀

added def DirichletCharacter.FactorsThrough

added theorem DirichletCharacter.changeLevel_eq_cast_of_dvd

added def DirichletCharacter.conductorSet

added theorem DirichletCharacter.level_mem_conductorSet

added theorem DirichletCharacter.mem_conductorSet_dvd

added theorem DirichletCharacter.mem_conductorSet_iff