aeval_homogenize_of_eq_one — Mathlib

English

Let A be a commutative semiring and an R-algebra of A. If natDegree p ≤ n, then MvPolynomial.aeval g (p.homogenize n) = p, for any g: Fin 2 → A with g(1) = 1.

Русский

Пусть A — коммутативное полуринг и алгебра над R в A. Если deg p ≤ n, тогда MvPolynomial.aeval g (p.homogenize n) = p для любого g: Fin 2 → A c g(1) = 1.

LaTeX

$$$\\forall p\\in R[X],\\; \\text{natDegree}(p) \\le n \\Rightarrow \\mathrm{aeval}\\, g\\, (p.homogenize\\ n) = p,$ где $g(1)=1$.$$

Lean4

theorem aeval_homogenize_of_eq_one {A : Type*} [CommSemiring A] [Algebra R A] {p : R[X]} {n : ℕ} (hn : natDegree p ≤ n)
    (g : Fin 2 → A) (hg : g 1 = 1) : MvPolynomial.aeval g (p.homogenize n) = aeval (g 0) p := by
  apply eval₂_homogenize_of_eq_one <;> assumption

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