isEllDivSequence_id

Mathlib.NumberTheory.EllipticDivisibilitySequence

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

English

The identity sequence id is an Elliptic Divisibility Sequence: IsEllDivSequence id.

Русский

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

LaTeX

$$$ IsEllDivSequence(id) $$$

Lean4

/-- The identity sequence is an EDS. -/
theorem isEllDivSequence_id : IsEllDivSequence id :=
  ⟨isEllSequence_id, isDivSequence_id⟩

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

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

Разделы

Аффилиация

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