ofJ0_c₄ — Mathlib

English

Let R be a commutative ring and W a Weierstrass curve over R. For the model with j-invariant 0, the coefficient c4 vanishes: c4 = 0.

Русский

Пусть R — коммутативное кольцо, W — кривой Вейершстраса над R. Для модели с инвариантой j равной 0 коэффициент c4 равен 0.

LaTeX

$$$$ (ofJ0 \; R).c_4 = 0 $$$$

Lean4

theorem ofJ0_c₄ : (ofJ0 R).c₄ = 0 := by
  rw [ofJ0, c₄, b₂, b₄]
  norm_num1

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