iterToSum_X

Mathlib.Algebra.MvPolynomial.Equiv

URI: https://scilib.ai/kg/mathlib#MvPolynomial.iterToSum_X

English

For any b in S1, iterToSum maps the indeterminate X b to X (Sum.inl b).

Русский

Для любого b∈S1 отображение iterToSum переводит X b в X(Sum.inl b).

LaTeX

$$$\operatorname{iterToSum} \;R\;S_1\;S_2\bigl(X b\bigr) = X\bigl(\mathrm{Sum.inl}\, b\bigr)$$$

Lean4

@[simp]
theorem iterToSum_X (b : S₁) : iterToSum R S₁ S₂ (X b) = X (Sum.inl b) :=
  eval₂_X _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru