natDegree_add_coeff_mul — Mathlib

English

natDegree_add_coeff_mul: (f · g).coeff (f.natDegree + g.natDegree) = f.coeff(f.natDegree) · g.coeff(g.natDegree).

Русский

коэффициент при степени f.natDegree + g.natDegree в произведении равно произведению соответствующих коэффициентов.

LaTeX

$$$\\bigl(f \\cdot g\\bigr).\\mathrm{coeff}\\bigl(f.\\mathrm{natDegree} + g.\\mathrm{natDegree}\\bigr) = f.\\mathrm{coeff}\\bigl(f.\\mathrm{natDegree}\\bigr) \\cdot g.\\mathrm{coeff}\\bigl(g.\\mathrm{natDegree}\\bigr)$$$

Lean4

theorem natDegree_add_coeff_mul (f g : R[X]) :
    (f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree := by
  simp only [coeff_natDegree, coeff_mul_degree_add_degree]

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