Odd

Mathlib.NumberTheory.DirichletCharacter.Basic

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

English

A Dirichlet character is odd if its value at -1 is -1.

Русский

Символ Дирихле нечетный, если его значение в -1 равняется -1.

LaTeX

$$$\\text{Odd} \\;\\psi := \\psi(-1) = -1.$$$

Lean4

/-- A Dirichlet character is odd if its value at -1 is -1. -/
def Odd : Prop :=
  ψ (-1) = -1

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

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

Разделы

Аффилиация

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