j_of_char_three

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.j_of_char_three

English

In characteristic three, for an elliptic Weierstrass curve W, j(W) equals Δ'^{-1} times b2^{6}.

Русский

В характеристике 3 для эллиптической кривой Вейерштрасса W: j(W) = Δ'^{-1} · b2^{6}.

LaTeX

$$$W.j = W.\Delta'^{-1} \cdot W.b_2^{6}$$$

Lean4

theorem j_of_char_three : W.j = W.Δ'⁻¹ * W.b₂ ^ 6 := by rw [j, W.c₄_of_char_three, ← pow_mul]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru