preΨ'_one — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preΨ'_one : W.preΨ' 1 = 1 :=
  preNormEDS'_one ..

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