variableChange_b₂

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

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

English

Under a linear change C, the b2 coefficient transforms as b2' = u^{-2} (b2 + 12 r).

Русский

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

LaTeX

$$$ (C \\cdot W).b_2 = C.u^{-2} \\big(W.b_2 + 12 C.r\\big). $$$

Lean4

theorem variableChange_b₂ : (C • W).b₂ = C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r) :=
  by
  simp only [b₂, variableChange_a₁, variableChange_a₂]
  ring1

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

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

Разделы

Аффилиация

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