leadingCoeff_preΨ — Mathlib

English

For any W and n with n ≠ 0 in R, the leading coefficient of W.preΨ n is (if Even n then n/2 else n).

Русский

Для любого W и n с n ≠ 0 в R ведущий коэффициент W.preΨ n равен (n/2) если n чётное, иначе n.

LaTeX

$$(W.preΨ n).leadingCoeff = \begin{cases} n/2, & \text{Even}(n) \\ n, & \text{not Even}(n) \end{cases}$$

Lean4

@[simp]
theorem leadingCoeff_preΨ {n : ℤ} (h : (n : R) ≠ 0) : (W.preΨ n).leadingCoeff = if Even n then n / 2 else n := by
  rw [leadingCoeff, W.natDegree_preΨ h, coeff_preΨ]

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