Commit 2023-09-21 01:54 18c578f6

View on Github →

feat: changeLevel for Dirichlet characters (#7263)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.castHom_comp

modified theorem ZMod.castHom_self

Created Mathlib/Data/ZMod/Units.lean

added def ZMod.unitsMap

added theorem ZMod.unitsMap_comp

added theorem ZMod.unitsMap_def

added theorem ZMod.unitsMap_self

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean

added theorem DirichletCharacter.changeLevel_def'

added theorem DirichletCharacter.changeLevel_def

added theorem DirichletCharacter.changeLevel_self

added theorem DirichletCharacter.changeLevel_self_toUnitHom

added theorem DirichletCharacter.changeLevel_trans

modified theorem DirichletCharacter.eval_modulus_sub

modified theorem DirichletCharacter.toUnitHom_eq_char'

modified theorem DirichletCharacter.toUnitHom_eq_iff