preNormEDS_neg

Mathlib.NumberTheory.EllipticDivisibilitySequence

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

English

For every n ∈ ℤ, preNormEDS(b,c,d)(-n) = - preNormEDS(b,c,d)(n).

Русский

Для каждого n ∈ ℤ выполняется preNormEDS(b,c,d)(-n) = - preNormEDS(b,c,d)(n).

LaTeX

$$$$\text{preNormEDS}(b,c,d)(-n) = -\text{preNormEDS}(b,c,d)(n).$$$$

Lean4

@[simp]
theorem preNormEDS_neg (n : ℤ) : preNormEDS b c d (-n) = -preNormEDS b c d n := by simp [preNormEDS]

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

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

Разделы

Аффилиация

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