ext_iff_degree_le — Mathlib

English

Let p, q ∈ R[X] and n ∈ ℕ with degree p ≤ n and degree q ≤ n. Then p = q if and only if p.coeff i = q.coeff i for all i ≤ n.

Русский

Пусть p, q ∈ R[X] и n ∈ ℕ, deg p ≤ n и deg q ≤ n. Тогда p = q тогда и только тогда, когда p.coeff i = q.coeff i для всех i ≤ n.

LaTeX

$$$ p, q \in R[X], n \in \mathbb{N},\; \deg p \le n, \deg q \le n \Rightarrow\; (p = q \iff \forall i \le n, p.coeff(i) = q.coeff(i)) $$$

Lean4

theorem ext_iff_degree_le {p q : R[X]} {n : ℕ} (hp : p.degree ≤ n) (hq : q.degree ≤ n) :
    p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i :=
  ext_iff_natDegree_le (natDegree_le_of_degree_le hp) (natDegree_le_of_degree_le hq)

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