preΨ'_four — Mathlib

English

Let W be a Weierstrass curve over a commutative ring. The univariate preΨ' at 4 equals preΨ₄: preΨ'(4) = preΨ₄.

Русский

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

LaTeX

$$$W.pre\\Psi'(4) = W.pre\\Psi_4$$$

Lean4

@[simp]
theorem preΨ'_four : W.preΨ' 4 = W.preΨ₄ :=
  preNormEDS'_four ..

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