normEDS_neg

Mathlib.NumberTheory.EllipticDivisibilitySequence

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

English

For every integer n, normEDS(b,c,d,-n) equals minus normEDS(b,c,d,n).

Русский

Для любого целого n выполняется равенство: normEDS(b,c,d,-n) = -normEDS(b,c,d,n).

LaTeX

$$$\operatorname{normEDS}(b,c,d,-n) = -\operatorname{normEDS}(b,c,d,n)$$$

Lean4

@[simp]
theorem normEDS_neg (n : ℤ) : normEDS b c d (-n) = -normEDS b c d n := by
  simp_rw [normEDS, preNormEDS_neg, even_neg, neg_mul]

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

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

Разделы

Аффилиация

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