ΨSq_even — Mathlib

English

Let W be a Weierstrass curve over a commutative ring. For every integer m, the even index of the ΨSq-polynomial on W is given by a specific square of a combination of preΨ values, times Ψ₂Sq.

Русский

Пусть W — это кривой Вейерштрасса над коммутативным кольцом. Для каждого целого m чётная величина ΨSq-полином на W задаётся как квадрат выражения, состоящего из значений preΨ, умноженного на Ψ₂Sq.

LaTeX

$$$W.\\ΨSq(2m) = \Bigl( W.preΨ(m-1)^2 \cdot W.preΨ(m) \cdot W.preΨ(m+2) - W.preΨ(m-2) \cdot W.preΨ(m) \cdot W.preΨ(m+1)^2 \Bigr)^2 \cdot W.\\Ψ₂Sq$$$

Lean4

theorem ΨSq_even (m : ℤ) :
    W.ΨSq (2 * m) =
      (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq :=
  by rw [ΨSq, preΨ_even, if_pos <| even_two_mul m]

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