ext_iff — Mathlib

English

Two polynomials are equal if and only if all their coefficients are equal: p = q ⇔ ∀ n, coeff p n = coeff q n.

Русский

Два полинома равны тогда и только тогда, когда их коэффициенты совпадают: p = q ⇔ ∀ n, coeff p n = coeff q n.

LaTeX

$$$p = q \iff \forall n, \operatorname{coeff}(p,n) = \operatorname{coeff}(q,n)$$$

Lean4

theorem ext_iff {p q : R[X]} : p = q ↔ ∀ n, coeff p n = coeff q n :=
  by
  rcases p with ⟨f : ℕ →₀ R⟩
  rcases q with ⟨g : ℕ →₀ R⟩
  simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)

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