aeval_homogenize_X_one — Mathlib

English

If natDegree p ≤ n, then MvPolynomial.aeval ![X,1] (p.homogenize n) = p.

Русский

При условии deg(p) ≤ n имеет место $\\mathrm{aeval}\\, ![X,1] (p.homogenize n) = p$.

LaTeX

$$$\\mathrm{aeval}\\, ![X,1]\\,(p.homogenize\\ n) = p \\quad\\text{если } \\operatorname{natDegree}(p) \\le n.$$$

Lean4

/-- If `deg p ≤ n`, then `homogenize p n (x, 1) = p x`. -/
@[simp]
theorem aeval_homogenize_X_one (p : R[X]) {n : ℕ} (hn : natDegree p ≤ n) :
    MvPolynomial.aeval ![X, 1] (p.homogenize n) = p := by rw [aeval_homogenize_of_eq_one] <;> simp [*]

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