Theorem DirichletCharacter.conductor_le_conductor_mem_conductorSet

Modification history

2023-11-23 10:43
Mathlib/NumberTheory/DirichletCharacter/Basic.lean
feat: reduction of DirichletCharacter (#8440)
Added DirichletCharacter.conductor_le_conductor_mem_conductorSetView on Github →