leadingCoeff_Φ — Mathlib

English

For a Weierstrass curve W over a nontrivial ring R, the leading coefficient of W.Φ(n) is 1 for every integer n.

Русский

Для кривая Вейерштрасса W над не тривиальным кольцом R ведущий коэффициент W.Φ(n) равен 1 для каждого целого n.

LaTeX

$$$(W.\Φ(n)).leadingCoeff = 1$$$

Lean4

@[simp]
theorem leadingCoeff_Φ [Nontrivial R] (n : ℤ) : (W.Φ n).leadingCoeff = 1 := by rw [leadingCoeff, natDegree_Φ, coeff_Φ]

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