c₆_of_isCharNeTwoNF — Mathlib

English

Let W be a Weierstrass curve over a commutative ring with characteristic not equal to 2. Then c6 equals minus 64 a2 cubed plus 288 a2 a4 minus 864 a6.

Русский

Пусть W — кривая Вейерштрасса над коммутативным кольцом, характеристика которого не равна 2. Тогда c6 равно -64 a2^3 + 288 a2 a4 - 864 a6.

LaTeX

$$$$ W.c_6 = -64 \cdot W.a_2^3 + 288 \cdot W.a_2 \cdot W.a_4 - 864 \cdot W.a_6 $$$$

Lean4

@[simp]
theorem c₆_of_isCharNeTwoNF : W.c₆ = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆ :=
  by
  rw [c₆, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF, b₆_of_isCharNeTwoNF]
  ring1

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