ext — Mathlib

English

Two multivariate polynomials are equal if all their coefficients agree; equality is determined coefficientwise.

Русский

Два многочлена по нескольким переменным равны тогда и только когда совпадают все их коэффициенты.

LaTeX

$$$\forall p,q:\ MvPolynomial\;\sigma\;R,\ (\forall m,\mathrm{coeff}(m,p)=\mathrm{coeff}(m,q)) \rightarrow p=q$$$

Lean4

@[ext]
theorem ext (p q : MvPolynomial σ R) : (∀ m, coeff m p = coeff m q) → p = q :=
  Finsupp.ext

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