preΨ'_zero — Mathlib

English

Let W be a Weierstrass curve over a commutative ring. The univariate auxiliary polynomial preΨ' evaluated at 0 is zero: preΨ'(0) = 0.

Русский

Пусть W — кривая Вейерштрасса над коммутативной кольцевой структурой. Внедренный до-вспомогательный многочлен preΨ' при аргументе 0 равен нулю: preΨ'(0) = 0.

LaTeX

$$$W.pre\\Psi'(0) = 0$$$

Lean4

@[simp]
theorem preΨ'_zero : W.preΨ' 0 = 0 :=
  preNormEDS'_zero ..

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