factorsThrough_one_iff — Mathlib

English

A Dirichlet character χ factors through level 1 if and only if χ is the trivial character.

Русский

Символ Дирихле χ факторизуется через уровень 1 тогда и только тогда, когда χ — тривиальный символ.

LaTeX

$$$\\operatorname{FactorsThrough}(\\chi,1) \\iff \\chi = 1$$$

Lean4

theorem factorsThrough_one_iff : FactorsThrough χ 1 ↔ χ = 1 :=
  by
  refine ⟨fun ⟨_, χ₀, hχ₀⟩ ↦ ?_, fun h ↦ ⟨one_dvd n, 1, by rw [h, changeLevel_one]⟩⟩
  rwa [level_one χ₀, changeLevel_one] at hχ₀

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