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