b₄_of_isCharNeTwoNF — Mathlib

English

Let W be a Weierstrass curve over a commutative ring with characteristic not equal to 2. Then b4 equals 2 a4.

Русский

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

LaTeX

$$$$ W.b_4 = 2 \cdot W.a_4 $$$$

Lean4

@[simp]
theorem b₄_of_isCharNeTwoNF : W.b₄ = 2 * W.a₄ :=
  by
  rw [b₄, a₃_of_isCharNeTwoNF]
  ring1

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