variableChange_c₄

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

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

English

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

Русский

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

LaTeX

$$$ (C \\cdot W).c_4 = C.u^{-4} W.c_4. $$$

Lean4

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

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

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

Разделы

Аффилиация

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