level_one

Mathlib.NumberTheory.DirichletCharacter.Basic

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

English

If χ is a Dirichlet character at level 1, then χ equals the trivial character 1.

Русский

Если χ — символ Дирихле уровня 1, то χ равен тривиальному символу 1.

LaTeX

$$$$ \\forall χ \\in \\operatorname{DirichletCharacter}(R,1),\\; χ = 1. $$$$

Lean4

theorem level_one (χ : DirichletCharacter R 1) : χ = 1 := by
  ext
  simp [units_eq_one]

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

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

Разделы

Аффилиация

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