mk — Mathlib · SciLib

English

For any polynomial x ∈ R[X], and y ∈ W'.CoordinateRing, x · y equals mk W' (C x) times y in the coordinate ring.

Русский

Для любого многочлена x ∈ R[X] и элемента y ∈ W'.CoordinateRing имеет место равенство x·y = mk W' (C x)·y.

LaTeX

$$$ x \in R[X],\ y \in W'.CoordinateRing:\ x \cdot y = mk W' (C x) \cdot y $$$

Lean4

/-- The natural ring homomorphism mapping `R[X][Y]` to `R[W]`. -/
noncomputable abbrev mk : R[X][Y] →+* W'.CoordinateRing :=
  AdjoinRoot.mk W'.polynomial

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