variableChange_a₁

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

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

English

Under a linear change C, the a1 coefficient transforms according to a simple linear expression: a1' = u^{-1} (a1 + 2 s).

Русский

При линейном преобразовании C коэффициент a1 получает новое значение: a1' = u^{-1}(a1 + 2 s).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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