Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-10-23 09:15
4a242ae6
View on Github →
feat: properties of the conductor (
#7352
)
Estimated changes
Modified
Mathlib/NumberTheory/DirichletCharacter/Basic.lean
added
theorem
DirichletCharacter.changeLevel_one
added
theorem
DirichletCharacter.conductor_dvd_level
added
theorem
DirichletCharacter.conductor_eq_zero_iff_level_eq_zero
added
theorem
DirichletCharacter.conductor_mem_conductorSet
added
theorem
DirichletCharacter.conductor_ne_zero
added
theorem
DirichletCharacter.conductor_one
added
theorem
DirichletCharacter.conductor_one_dvd
added
theorem
DirichletCharacter.eq_one_iff_conductor_eq_one
added
theorem
DirichletCharacter.factorsThrough_conductor
added
theorem
DirichletCharacter.factorsThrough_one_iff
added
def
DirichletCharacter.isPrimitive
added
theorem
DirichletCharacter.isPrimitive_def
added
theorem
DirichletCharacter.isPrimitive_one_level_one
added
theorem
DirichletCharacter.isPritive_one_level_zero
added
theorem
DirichletCharacter.level_one'
added
theorem
DirichletCharacter.level_one