j_eq_zero_iff_of_char_two' — Mathlib

English

In characteristic two without any reducedness assumption, j = 0 if and only if a1^{12} = 0.

Русский

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

LaTeX

$$$W.j = 0 \iff W.a_1^{12} = 0$$$

Lean4

/-- A variant of `WeierstrassCurve.j_eq_zero_iff_of_char_two` without assuming a reduced ring. -/
theorem j_eq_zero_iff_of_char_two' : W.j = 0 ↔ W.a₁ ^ 12 = 0 := by rw [j_of_char_two, Units.mul_right_eq_zero]

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