ModelOfHasCoeffs — Mathlib

English

The model of S over a ring R0 containing the coefficients of P is the polynomial ring over R0 in ι variables, modulo the ideal generated by the relations of HasCoeffs.

Русский

Модель S над кольцом R0, содержащим коэффициенты P, равна кольцу Р0[X_i] по i ∈ ι, деленному по идеалу, сгенерированному отношениями HasCoeffs.

LaTeX

$$$\\mathrm{ModelOfHasCoeffs} :\\;=MvPolynomial_{\\iota} R_0 \\big/ \\langle \\mathrm{range}(P.\\mathrm{relationOfHasCoeffs}\\,R_0)\\rangle$$$

Lean4

/-- The model of `S` over a `R₀` that contains the coefficients of `P` is `R₀[X]` quotiented by the
same relations. -/
abbrev ModelOfHasCoeffs : Type _ :=
  MvPolynomial ι R₀ ⧸ (Ideal.span <| Set.range (P.relationOfHasCoeffs R₀))

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