coeff_add_eq_left_of_lt — Mathlib

English

If q has smaller natDegree than n, then the coefficient of n in p+q is the same as the coefficient of n in p.

Русский

Если natDegree(q) < n, то коэффициент при x^n в p+q равен коэффициенту при x^n в p.

LaTeX

$$$\operatorname{natDegree}(q) < n \Rightarrow (p + q).\coeff(n) = p.\coeff(n)$$$

Lean4

theorem coeff_add_eq_left_of_lt (qn : q.natDegree < n) : (p + q).coeff n = p.coeff n :=
  (coeff_add _ _ _).trans <| (congr_arg _ <| coeff_eq_zero_of_natDegree_lt <| qn).trans <| add_zero _

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