aeval_val_relationOfHasCoeffs — Mathlib

English

The relationOfHasCoeffs maps to the presentation relation via algebraMap, establishing compatibility.

Русский

relationOfHasCoeffs отображается в P.relation через алгебра Map, обеспечивая совместимость.

LaTeX

$$$\\mathrm{MvPolynomial}.map(\\mathrm{algebraMap}\\,R_0\\,R)(P.relationOfHasCoeffs\\,R_0\\,r) = P.relation\\,r$$$

Lean4

@[simp]
theorem aeval_val_relationOfHasCoeffs (r : σ) : MvPolynomial.aeval P.val (P.relationOfHasCoeffs R₀ r) = 0 := by
  rw [← MvPolynomial.aeval_map_algebraMap R, map_relationOfHasCoeffs, aeval_val_relation]

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