j_eq_zero_iff — Mathlib

English

Let W be a Weierstrass curve over a reduced commutative ring R, and suppose W is elliptic. Then the j-invariant vanishes exactly when the invariant c4 vanishes:

Русский

Пусть W — кривая Вейерштрасса над редуцированным кольцом R и W является эллиптической. Тогда j-инвариант обращается в 0 тогда и только тогда, когда c4 равен 0.

LaTeX

$$$W\;j = 0 \iff W\;c_4 = 0$$$

Lean4

theorem j_eq_zero_iff [IsReduced R] : W.j = 0 ↔ W.c₄ = 0 := by
  rw [j_eq_zero_iff', IsReduced.pow_eq_zero_iff three_ne_zero]

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