delta

Mathlib.NumberTheory.LSeries.Basic

URI: https://scilib.ai/kg/mathlib#LSeries.delta

English

The indicator function δ selects n = 1 with value 1, otherwise 0.

Русский

Индикаторная функция δ выбирает n = 1 и равна 1, иначе 0.

LaTeX

$$δ(n) = \begin{cases}1,& n=1\\0,& n\neq 1\end{cases}$$

Lean4

/-- The indicator function of `{1} ⊆ ℕ` with values in `ℂ`. -/
def delta (n : ℕ) : ℂ :=
  if n = 1 then 1 else 0

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

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

Разделы

Аффилиация

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