Theorem DirichletCharacter.zero_ne_mem_conductorSet

Modification history

2026-04-03 09:00

Mathlib/NumberTheory/DirichletCharacter/Basic.lean

chore(NumberTheory/DirichletCharacter): use [NeZero n] everywhere (#37425) …

Modified DirichletCharacter.zero_ne_mem_conductorSet View on Github →

2026-01-30 09:16

Mathlib/NumberTheory/DirichletCharacter/Basic.lean

feat(DirichletCharacter): any element of the `conductorSet` is divisible by the conductor (#34569) …

Added DirichletCharacter.zero_ne_mem_conductorSet View on Github →