rename_polynomial_aeval_X — Mathlib

English

Same as NatDegree FinSucc; the natDegree of the finSuccEquiv image equals the original degree with respect to the 0-th variable.

Русский

То же самое, что и NatDegree FinSucc; натуральная степень образа finSuccEquiv равна исходной степени по 0-й переменной.

LaTeX

$$$\mathrm{natDegree}(\mathrm{finSuccEquiv}(R,n)\,f) = \deg_0 f$$$

Lean4

@[simp]
theorem rename_polynomial_aeval_X {σ τ : Type*} (f : σ → τ) (i : σ) (p : R[X]) :
    rename f (Polynomial.aeval (X i) p) = Polynomial.aeval (X (f i) : MvPolynomial τ R) p := by
  rw [← aeval_algHom_apply, rename_X]

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