j_of_isShortNF_of_char_three — Mathlib

English

If the base field has characteristic 3, then the j-invariant of a Weierstrass curve in short NF is zero.

Русский

Если характеристика поля равна 3, то j-инварианта кривая Вейерштрасса в краткой нормальной форме равна нулю.

LaTeX

$$$ j(W) = 0 \quad\text{when characteristic}(F) = 3 $$$

Lean4

@[simp]
theorem j_of_isShortNF_of_char_three [CharP F 3] : W.j = 0 := by rw [j, c₄_of_isShortNF_of_char_three]; simp

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