IsEllDivSequence

Mathlib.NumberTheory.EllipticDivisibilitySequence

URI: https://scilib.ai/kg/mathlib#IsEllDivSequence

English

The identity sequence id is an Elliptic Divisibility Sequence.

Русский

Идиентическая последовательность id является Эллиптической Последовательностью Делимости.

LaTeX

$$$ IsEllDivSequence(id) $$$

Lean4

/-- The proposition that a sequence indexed by integers is an EDS. -/
def IsEllDivSequence : Prop :=
  IsEllSequence W ∧ IsDivSequence W

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

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

Разделы

Аффилиация

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