commAlgEquiv_C_X

Mathlib.Algebra.MvPolynomial.Equiv

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

English

Under the commAlgEquiv, the element C(X i) is mapped to the X i in the target algebra.

Русский

Под commAlgEquiv элемент C(X i) переходит в X i в целевой алгебре.

LaTeX

$$$\text{commAlgEquiv} \;\_\; (C(X i)) = X i$$$

Lean4

theorem commAlgEquiv_C_X (i) : commAlgEquiv R S₁ S₂ (.C (.X i)) = .X i := by simp

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

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

Разделы

Аффилиация

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