variableChange_a₃

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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