relationOfHasCoeffs — Mathlib

English

The map of relationOfHasCoeffs through algebraMap from R0 to R lands in the original relation P.relation.

Русский

Образ relationOfHasCoeffs через алгебра map из R0 в R лежит в исходном отношении P.relation.

LaTeX

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

Lean4

/-- The `r`-th relation of `P` as a polynomial in `R₀`. This is the (arbitrary) choice of a
pre-image under the map `R₀[X] → R[X]`. -/
noncomputable def relationOfHasCoeffs (r : σ) : MvPolynomial ι R₀ :=
  (HasCoeffs.relation_mem_range_map (P := P) R₀ r).choose

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