j_of_char_two

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

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

English

In characteristic two, for an elliptic Weierstrass curve W, the j-invariant equals Δ'^{-1} times a1^{12}.

Русский

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

LaTeX

$$$W.j = W.\Delta'^{-1} \cdot W.a_1^{12}$$$

Lean4

theorem j_of_char_two : W.j = W.Δ'⁻¹ * W.a₁ ^ 12 := by rw [j, W.c₄_of_char_two, ← pow_mul]

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

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

Разделы

Аффилиация

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