smeval_assoc_X_pow — Mathlib

English

For p ∈ R[X], m,n ∈ ℕ, smeval respects the associative rearrangement X^m · (X^n · p) = (X^m · X^n) · p in the smeval sense: p.smeval x · x^m · x^n = p.smeval x · (x^m · x^n).

Русский

Для p ∈ R[X], m,n ∈ ℕ, smeval сохраняет ассоциативность в выражении X^m · (X^n · p): p.smeval x · x^m · x^n = p.smeval x · (x^m · x^n).

LaTeX

$$$$ p.smeval x \cdot x^m \cdot x^n = p.smeval x \cdot (x^m \cdot x^n). $$$$

Lean4

theorem smeval_assoc_X_pow (m n : ℕ) : p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n) := by
  induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [smeval_add, ph, qh, add_mul]
  | monomial n a => rw [smeval_monomial, smul_mul_assoc, smul_mul_assoc, npow_mul_assoc, ← smul_mul_assoc]

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