b₈_of_isCharNeTwoNF — Mathlib

English

Let W be a Weierstrass curve over a commutative ring with characteristic not equal to 2. Then b8 equals 4 a2 a6 minus a4 squared.

Русский

Пусть W — кривая Вейерштрасса над коммутативным кольцом, характеристика которого не равна 2. Тогда b8 равно 4 a2 a6 минус a4 в квадрате.

LaTeX

$$$$ W.b_8 = 4 \cdot W.a_2 \cdot W.a_6 - W.a_4^2 $$$$

Lean4

@[simp]
theorem b₈_of_isCharNeTwoNF : W.b₈ = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2 :=
  by
  rw [b₈, a₁_of_isCharNeTwoNF, a₃_of_isCharNeTwoNF]
  ring1

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