variableChange_c₆

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.variableChange_c₆

English

Under a linear change C, the c6 coefficient scales by u^{-6}: c6' = u^{-6} c6.

Русский

При линейном преобразовании C коэффициент c6 масштабируется как c6' = u^{-6} c6.

LaTeX

$$$ (C \\cdot W).c_6 = C.u^{-6} W.c_6. $$$

Lean4

theorem variableChange_c₆ : (C • W).c₆ = C.u⁻¹ ^ 6 * W.c₆ :=
  by
  simp only [c₆, variableChange_b₂, variableChange_b₄, variableChange_b₆]
  ring1

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

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

Разделы

Аффилиация

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