c₄_of_isCharNeTwoNF — Mathlib

English

Let W be a Weierstrass curve over a commutative ring with characteristic not equal to 2. Then c4 equals 16 a2 squared minus 48 a4.

Русский

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

LaTeX

$$$$ W.c_4 = 16 \cdot W.a_2^2 - 48 \cdot W.a_4 $$$$

Lean4

@[simp]
theorem c₄_of_isCharNeTwoNF : W.c₄ = 16 * W.a₂ ^ 2 - 48 * W.a₄ :=
  by
  rw [c₄, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF]
  ring1

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