map_relationOfHasCoeffs — Mathlib

English

The coefficient spread of relationOfHasCoeffs maps to the corresponding relation under the base map.

Русский

Распространение коэффициентов relationOfHasCoeffs отображается в соответствующее отношение под основанным отображением.

LaTeX

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

Lean4

theorem map_relationOfHasCoeffs (r : σ) :
    MvPolynomial.map (algebraMap R₀ R) (P.relationOfHasCoeffs R₀ r) = P.relation r :=
  (HasCoeffs.relation_mem_range_map R₀ r).choose_spec

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