preΨ_neg

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.preΨ_neg

English

For any Weierstrass curve W and any integer n, preΨ(-n) = - preΨ(n).

Русский

Для любой кривой Вейерштрасса W и любого целого числа n выполняется равенство: preΨ(-n) = - preΨ(n).

LaTeX

$$$W.pre\\Psi(-n) = -W.pre\\Psi(n)$$$

Lean4

@[simp]
theorem preΨ_neg (n : ℤ) : W.preΨ (-n) = -W.preΨ n :=
  preNormEDS_neg ..

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

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

Разделы

Аффилиация

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