Δ_of_isCharNeTwoNF — Mathlib

English

Let W be a Weierstrass curve over a commutative ring with characteristic not equal to 2. Then the discriminant Δ equals a specific polynomial in a2, a4, a6.

Русский

Пусть W — кривая Вейерштрасса над коммутативным кольцом, характеристика которого не равна 2. Тогда дискриминант Δ выражается через коэффициенты a2, a4 и a6 по определённому многочлену.

LaTeX

$$$$ W.\Delta = -64 \cdot W.a_2^3 \cdot W.a_6 + 16 \cdot W.a_2^2 \cdot W.a_4^2 - 64 \cdot W.a_4^3 - 432 \cdot W.a_6^2 + 288 \cdot W.a_2 \cdot W.a_4 \cdot W.a_6 $$$$

Lean4

@[simp]
theorem Δ_of_isCharNeTwoNF :
    W.Δ =
      -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆ :=
  by
  rw [Δ, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF, b₆_of_isCharNeTwoNF, b₈_of_isCharNeTwoNF]
  ring1

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