IsPrimitive

Mathlib.NumberTheory.DirichletCharacter.Basic

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

English

A character is primitive if its level equals its conductor.

Русский

Символ примитивен тогда и только тогда, когда его уровень равен кондуктору.

LaTeX

$$$\text{IsPrimitive}(\\chi) \iff \\operatorname{conductor}(\\chi) = n$$$

Lean4

/-- A character is primitive if its level is equal to its conductor. -/
def IsPrimitive : Prop :=
  conductor χ = n

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

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

Разделы

Аффилиация

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