primitiveCharacter_one — Mathlib

English

The primitiveCharacter of the trivial character at level n equals 1.

Русский

ПримитивныйCharacter тривиального символа на уровне n равен 1.

LaTeX

$$$(\\mathrm{DirichletCharacter}(R,n).\\operatorname{primitiveCharacter})(1) = 1$$$

Lean4

theorem primitiveCharacter_one (hn : n ≠ 0) : (1 : DirichletCharacter R n).primitiveCharacter = 1 := by
  rw [eq_one_iff_conductor_eq_one <| (@conductor_one R _ _ hn) ▸ Nat.one_ne_zero,
    (isPrimitive_def _).1 (1 : DirichletCharacter R n).primitiveCharacter_isPrimitive, conductor_one hn]

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