Commit 2026-04-03 09:00 79463c83

View on Github →

chore(NumberTheory/DirichletCharacter): use [NeZero n] everywhere (#37425) At the moment, both n ≠ 0 and [NeZero n] are used in the file Mathlib.NumberTheory.DirichletCharacter.Basic to express the fact that the level is nonzero. This PR fixes that by changing to [NeZero n] everywhere.

Estimated changes

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean

modified theorem DirichletCharacter.changeLevel_eq_one_iff

modified theorem DirichletCharacter.conductor_dvd_of_mem_conductorSet

modified theorem DirichletCharacter.conductor_ne_zero

modified theorem DirichletCharacter.conductor_one

modified theorem DirichletCharacter.eq_one_iff_conductor_eq_one

modified theorem DirichletCharacter.primitiveCharacter_one

modified theorem DirichletCharacter.zero_ne_mem_conductorSet

Modified Mathlib/NumberTheory/LSeries/DirichletContinuation.lean