coeff_inj — Mathlib

English

The map that sends a polynomial to its sequence of coefficients is injective: two polynomials are equal if and only if all their coefficients agree.

Русский

Отображение, отправляющее многочлен в последовательность его коэффициентов, инъективно: два многочлена равны тогда и только тогда, когда совпадают все их коэффициенты.

LaTeX

$$$ p = q \\iff \\forall n, p.coeff(n) = q.coeff(n) $$$

Lean4

@[simp]
theorem coeff_inj : p.coeff = q.coeff ↔ p = q :=
  coeff_injective.eq_iff

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