coeff_homogenize — Mathlib

English

Let p ∈ R[X], n ∈ ℕ and m: Fin 2 →₀ ℕ be a 2-index exponent. Then the coefficient of m in (homogenize p n) is p_{m0} if m0 + m1 = n, and 0 otherwise.

Русский

Пусть p ∈ R[X], n ∈ ℕ и m: Fin 2 → ℕ — двухиндексная степень. Коэффициент при m в (homogenize p n) равен p_{m0} если m0 + m1 = n, и равен 0 иначе.

LaTeX

$$$(\\operatorname{homogenize} p\\, n)_{m} = \\begin{cases} p_{m_0}, & m_0 + m_1 = n, \\\\ 0, & \\text{иначе}. \\end{cases}$$$

Lean4

theorem coeff_homogenize (p : R[X]) (n : ℕ) (m : Fin 2 →₀ ℕ) :
    (homogenize p n).coeff m = if m 0 + m 1 = n then coeff p (m 0) else 0 := by
  induction p using Polynomial.induction_on' with
  | add p q ihp ihq => simp [*, ite_add_ite]
  | monomial k c =>
    rcases le_or_gt k n with hkn | hnk
    · rw [homogenize_monomial hkn, coeff_monomial, MvPolynomial.coeff_monomial]
      have : (fun₀ | 0 => m 0 | 1 => m 1) = m := by ext i; fin_cases i <;> simp
      aesop
    · aesop (add simp homogenize_monomial_of_lt) (add simp coeff_monomial)

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