isEllSequence_id

Mathlib.NumberTheory.EllipticDivisibilitySequence

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

English

The identity sequence id is an elliptic sequence for W: ℤ → ℤ.

Русский

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

LaTeX

$$$ IsEllSequence(id) $$$

Lean4

theorem isEllSequence_id : IsEllSequence id := fun _ _ _ => by simp_rw [id_eq]; ring1

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

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

Разделы

Аффилиация

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