b_relation

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.b_relation

English

The basic Weierstrass coefficients satisfy the fundamental relation 4 b8 = b2 b6 − b4^2.

Русский

Базовые коэффициенты Вейерштрасса удовлетворяют основному соотношению 4 b8 = b2 b6 − b4^2.

LaTeX

$$$$ 4 \cdot W.b_8 = W.b_2 \cdot W.b_6 - W.b_4^2 $$$$

Lean4

theorem b_relation : 4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2 :=
  by
  simp only [b₂, b₄, b₆, b₈]
  ring1

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

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

Разделы

Аффилиация

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