coeff_eq — Mathlib

English

If p and q are monic of the same degree n, then for all m ≥ n, the coefficients satisfy p.coeff(m) = q.coeff(m).

Русский

Если p и q монические степени n, то для всех m ≥ n коэффициенты совпадают: p.coeff(m) = q.coeff(m).

LaTeX

$$$\forall p,q:\; p.IsMonicOfDegree(n) \land q.IsMonicOfDegree(n) \Rightarrow \forall m \ge n,\; p.coeff(m) = q.coeff(m)$$$

Lean4

theorem coeff_eq {p q : R[X]} {n : ℕ} (hp : IsMonicOfDegree p n) (hq : IsMonicOfDegree q n) {m : ℕ} (hm : n ≤ m) :
    p.coeff m = q.coeff m := by
  nontriviality R
  rw [isMonicOfDegree_iff] at hp hq
  rcases eq_or_lt_of_le hm with rfl | hm
  · rw [hp.2, hq.2]
  · replace hp : p.natDegree < m := hp.1.trans_lt hm
    replace hq : q.natDegree < m := hq.1.trans_lt hm
    rw [coeff_eq_zero_of_natDegree_lt hp, coeff_eq_zero_of_natDegree_lt hq]

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