conductor_eq_zero_iff_level_eq_zero

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.conductor_eq_zero_iff_level_eq_zero

← MathLib Explorer

English

Conductor χ equals 0 iff n = 0.

Русский

Conductor χ равен 0 тогда и только тогда, когда n = 0.

LaTeX

$$$\\operatorname{conductor}(\\chi) = 0 \\iff n = 0$$$

Lean4

theorem conductor_eq_zero_iff_level_eq_zero : conductor χ = 0 ↔ n = 0 :=
  by
  refine ⟨(conductor_ne_zero χ).mtr, ?_⟩
  rintro rfl
  exact Nat.sInf_eq_zero.mpr <| Or.inl <| level_mem_conductorSet χ

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru