sumToIter_Xr — Mathlib

English

Let R be a commutative semiring and S1, S2 types. The map sumToIter sends the multivariate indeterminate X on the right component (Sum.inr c) to the coefficient-embedding of X c: sumToIter(R, S1, S2)(X(Sum.inr c)) = C(X c) for every c ∈ S2.

Русский

Пусть R — коммутативная полукольцо, S1, S2 — множества. Отображение sumToIter переводит переменную X, лежащую в правой части, в константный полином: sumToIter(R, S1, S2)(X(Sum.inr c)) = C(X c) для всякого c∈S2.

LaTeX

$$$\operatorname{sumToIter} \;R\;S_1\;S_2\bigl(X(\mathrm{Sum.inr}\, c)\bigr) = C\bigl(X c\bigr)$$$

Lean4

@[simp]
theorem sumToIter_Xr (c : S₂) : sumToIter R S₁ S₂ (X (Sum.inr c)) = C (X c) :=
  eval₂_X _ _ (Sum.inr c)

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