leadingCoeff_ΨSq — Mathlib

English

Let W be a Weierstrass curve over a Noetherian ring R with (n : R) ≠ 0. The leading coefficient of the polynomial W.ΨSq(n) equals n^2.

Русский

Пусть W — кривая Вейерштрасса над кольцом R с условием (n : R) ≠ 0. Ведущий коэффициент полинома W.ΨSq(n) равен n^2.

LaTeX

$$$\operatorname{leadingCoeff}\bigl(W.\PsiSq(n)\bigr) = n^2$$$

Lean4

@[simp]
theorem leadingCoeff_ΨSq [NoZeroDivisors R] {n : ℤ} (h : (n : R) ≠ 0) : (W.ΨSq n).leadingCoeff = n ^ 2 := by
  rw [leadingCoeff, W.natDegree_ΨSq h, coeff_ΨSq]

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