az

Mathlib.NumberTheory.PellMatiyasevic

URI: https://scilib.ai/kg/mathlib#Pell.az

English

For every a with a > 1, az(a) is the integer equal to a.

Русский

Пусть a ∈ ℕ и a > 1. Тогда az(a) — это целое число, равное a.

LaTeX

$$$ az(a) = a $$$

Lean4

/-- The element `a` such that `d = a ^ 2 - 1`, considered as an integer. -/
def az (a : ℕ) : ℤ :=
  a

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

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

Разделы

Аффилиация

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