conductor_one — Mathlib

English

If n ≠ 0 then conductor (1 : DirichletCharacter R n) = 1.

Русский

Если n ≠ 0, то conductor(1 : DirichletCharacter R n) = 1.

LaTeX

$$$n \neq 0 \Rightarrow \operatorname{conductor}(1 : \mathrm{DirichletCharacter}(R,n)) = 1$$$

Lean4

/-- The conductor of the trivial character is 1. -/
theorem conductor_one (hn : n ≠ 0) : conductor (1 : DirichletCharacter R n) = 1 :=
  by
  suffices FactorsThrough (1 : DirichletCharacter R n) 1
    by
    have h : conductor (1 : DirichletCharacter R n) ≤ 1 := Nat.sInf_le <| (mem_conductorSet_iff _).mpr this
    exact Nat.le_antisymm h (Nat.pos_of_ne_zero <| conductor_ne_zero _ hn)
  exact (factorsThrough_one_iff _).mpr rfl

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