eq_one_iff_conductor_eq_one — Mathlib

English

For n ≠ 0, χ = 1 iff conductor χ = 1.

Русский

Для n ≠ 0, χ = 1 тогда и только тогда, когда conductor χ = 1.

LaTeX

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

Lean4

theorem eq_one_iff_conductor_eq_one (hn : n ≠ 0) : χ = 1 ↔ conductor χ = 1 :=
  by
  refine ⟨fun h ↦ h ▸ conductor_one hn, fun hχ ↦ ?_⟩
  obtain ⟨h', χ₀, h⟩ := factorsThrough_conductor χ
  exact (level_one' χ₀ hχ ▸ h).trans <| changeLevel_one h'

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