eval₂_C_X — Mathlib

English

If φ(monomial n c) has natDegree fu(n) with fu(n) = n, then for every polynomial p, (φ p).natDegree = p.natDegree.

Русский

Если natDegree мономома φ(monomial n c) равен n, то для любого полинома p natDegree сохраняется: (φ p).natDegree = p.natDegree.

LaTeX

$$$ (\\phi p).natDegree = p.natDegree $$$

Lean4

@[simp]
theorem eval₂_C_X : eval₂ C X p = p :=
  Polynomial.induction_on' p (fun p q hp hq => by simp [hp, hq]) fun n x => by
    rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']

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