b_relation_of_char_three

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

English

Let W be a Weierstrass curve over a ring of characteristic 3. Then b_8 = b_2 b_6 − b_4^2.

Русский

Пусть W — кривая Вейерштрасса над кольцом с характеристикой 3. Тогда b_8 = b_2 b_6 − b_4^2.

LaTeX

$$$ b_8 = b_2 b_6 - b_4^2 $$$

Lean4

theorem b_relation_of_char_three : W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2 := by
  linear_combination W.b_relation - W.b₈ * CharP.cast_eq_zero R 3

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

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

Разделы

Аффилиация

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