variableChange_a₂

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.variableChange_a₂

English

Under a linear change C, the a2 coefficient transforms as a2' = u^{-2} (a2 - s a1 + 3 r - s^2).

Русский

При линейном преобразовании C коэффициент a2 переходит в a2' = u^{-2} (a2 - s a1 + 3 r - s^2).

LaTeX

$$$ (C \\cdot W).a_2 = C.u^{-2} \\big(W.a_2 - C.s W.a_1 + 3 C.r - C.s^2\\big). $$$

Lean4

theorem variableChange_a₂ : (C • W).a₂ = C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2) :=
  rfl

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

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

Разделы

Аффилиация

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