English
Let p ∈ R[X], q ∈ S[X], n ∈ ℕ with natDegree p ≤ n and natDegree q ≤ n. Then p = q if and only if p.coeff i = q.coeff i for all i ≤ n.
Русский
Пусть p ∈ R[X], q ∈ S[X], n ∈ ℕ, natDegree p ≤ n, natDegree q ≤ n. Тогда p = q тогда и только тогда, когда p.coeff i = q.coeff i для всех i ≤ n.
LaTeX
$$$ p \in R[X], q \in S[X], n \in \mathbb{N},\; \operatorname{natDegree}(p) \le n, \operatorname{natDegree}(q) \le n \Rightarrow\; (p = q \iff \forall i \le n, p.coeff(i) = q.coeff(i)) $$$
Lean4
theorem ext_iff_natDegree_le {p q : R[X]} {n : ℕ} (hp : p.natDegree ≤ n) (hq : q.natDegree ≤ n) :
p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i :=
by
refine Iff.trans Polynomial.ext_iff ?_
refine forall_congr' fun i => ⟨fun h _ => h, fun h => ?_⟩
refine (le_or_gt i n).elim h fun k => ?_
exact (coeff_eq_zero_of_natDegree_lt (hp.trans_lt k)).trans (coeff_eq_zero_of_natDegree_lt (hq.trans_lt k)).symm
