j_eq_zero_iff_of_char_three' — Mathlib

English

In characteristic three, without reducedness assumptions, j = 0 if and only if b2^{6} = 0.

Русский

В характеристике 3 без предположения о редуцированности: j = 0 тогда и только тогда, когда b2^{6} = 0.

LaTeX

$$$W.j = 0 \iff W.b_2^{6} = 0$$$

Lean4

/-- A variant of `WeierstrassCurve.j_eq_zero_iff_of_char_three` without assuming a reduced ring. -/
theorem j_eq_zero_iff_of_char_three' : W.j = 0 ↔ W.b₂ ^ 6 = 0 := by rw [j_of_char_three, Units.mul_right_eq_zero]

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