Δ_of_isCharTwoJEqZeroNF

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF

← MathLib Explorer

English

The discriminant Δ is given by Δ = -(64 a4^3 + 27 b6^2).

Русский

Дискриминант Δ задаётся как Δ = -(64 a4^3 + 27 b6^2).

LaTeX

$$$W.\Delta = -(64 \; W.a_4^{3} + 27 \; W.b_6^{2})$$$

Lean4

@[simp]
theorem Δ_of_isCharTwoJEqZeroNF : W.Δ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) :=
  by
  rw [Δ, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]
  ring1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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