English
For polynomials p, q over a semiring R, the coefficient at the combined trailing degree of the product equals the product of the trailing coefficients: (p q).coeff(p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff · q.trailingCoeff.
Русский
Для многочленов p, q над полукольцом R коэффициент при сумме их наихудших степеней равен произведению хвостовых коэффициентов: (p q).coeff(p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff · q.trailingCoeff.
LaTeX
$$$ (p * q).\text{coeff} (p.\\natTrailingDegree + q.\\natTrailingDegree) = p.\\trailingCoeff \cdot q.\\trailingCoeff $$$
Lean4
theorem coeff_mul_natTrailingDegree_add_natTrailingDegree :
(p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff :=
by
rw [coeff_mul]
refine Finset.sum_eq_single (p.natTrailingDegree, q.natTrailingDegree) ?_ fun h => (h (mem_antidiagonal.mpr rfl)).elim
rintro ⟨i, j⟩ h₁ h₂
rw [mem_antidiagonal] at h₁
by_cases hi : i < p.natTrailingDegree
· rw [coeff_eq_zero_of_lt_natTrailingDegree hi, zero_mul]
by_cases hj : j < q.natTrailingDegree
· rw [coeff_eq_zero_of_lt_natTrailingDegree hj, mul_zero]
rw [not_lt] at hi hj
refine (h₂ (Prod.ext_iff.mpr ?_).symm).elim
exact (add_eq_add_iff_eq_and_eq hi hj).mp h₁.symm
