j_eq_zero_iff' — Mathlib

English

For a Weierstrass curve W over a commutative ring with an elliptic structure, W.j = 0 if and only if W.c4^3 = 0.

Русский

Для кривой Вейерштрасса W над кольцом с эллиптической структурой, W.j = 0 тогда и только тогда, когда W.c4^3 = 0.

LaTeX

$$$ W.j = 0 \iff W.c_4^3 = 0 $$$

Lean4

/-- A variant of `WeierstrassCurve.j_eq_zero_iff` without assuming a reduced ring. -/
theorem j_eq_zero_iff' : W.j = 0 ↔ W.c₄ ^ 3 = 0 := by rw [j, Units.mul_right_eq_zero]

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