ΨSq_neg

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

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

English

The univariate ΨSq is an even function: ΨSq(-n) = ΨSq(n) for all integers n.

Русский

Одночлен ΨSq — чётная функция: ΨSq(-n) = ΨSq(n) для всех целых n.

LaTeX

$$$W.\\PsiSq(-n) = W.\\PsiSq(n)$$$

Lean4

@[simp]
theorem ΨSq_neg (n : ℤ) : W.ΨSq (-n) = W.ΨSq n := by simp [ΨSq]

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

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

Разделы

Аффилиация

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