coeff_pow_eq_ite_of_natDegree_le_of_le

English

Let o be a natural number. If natDegree(p) ≤ n, and m n ≤ o, then (p^m).coeff(o) equals (coeff p at n)^m if o = m n, and 0 otherwise.

Русский

Пусть o ∈ ℕ. Если natDegree(p) ≤ n и m n ≤ o, то (p^m).coeff(o) равно (coeff p n)^m, если o = m n, иначе 0.

LaTeX

$$$ (\operatorname{natDegree}(p) \le n) \Rightarrow (p^{m}).\coeff(o) = \text{if } o = m n \text{ then } (\operatorname{coeff} p n)^{m} \text{ else } 0 $$$

Lean4

theorem coeff_pow_eq_ite_of_natDegree_le_of_le {o : ℕ} (pn : natDegree p ≤ n) (mno : m * n ≤ o) :
    coeff (p ^ m) o = if o = m * n then (coeff p n) ^ m else 0 :=
  by
  rcases eq_or_ne o (m * n) with rfl | h
  · simpa only [ite_true] using coeff_pow_of_natDegree_le pn
  ·
    simpa only [h, ite_false] using
      coeff_eq_zero_of_natDegree_lt <| lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)

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