isPrimitive_one_level_zero

Mathlib.NumberTheory.DirichletCharacter.Basic

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

English

The Dirichlet character 1 at level 0 is primitive.

Русский

Символ Дирихле 1 на уровне 0 примитивен.

LaTeX

$$$\\text{IsPrimitive} \\left(1 : \mathrm{DirichletCharacter}(R,0)\\right)$$$

Lean4

theorem isPrimitive_one_level_zero : IsPrimitive (1 : DirichletCharacter R 0) :=
  conductor_eq_zero_iff_level_eq_zero.mpr rfl

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

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

Разделы

Аффилиация

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