complEDS_ofNat

Mathlib.NumberTheory.EllipticDivisibilitySequence

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

← MathLib Explorer

English

For natural n, the value of complEDS(b,c,d,k,n) equals complEDS'(b,c,d,k,n).

Русский

Для натурального n: complEDS(b,c,d,k,n) = complEDS'(b,c,d,k,n).

LaTeX

$$$\operatorname{complEDS}(b,c,d,k,n) = \operatorname{complEDS}'(b,c,d,k,n)$$$

Lean4

@[simp]
theorem complEDS_ofNat (n : ℕ) : complEDS b c d k n = complEDS' b c d k n :=
  by
  by_cases hn : n = 0
  · simp [hn, complEDS]
  · simp [complEDS, Int.sign_natCast_of_ne_zero hn]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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