commAlgEquiv_X

Mathlib.Algebra.MvPolynomial.Equiv

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

English

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

Русский

Под commAlgEquiv X i отображается в C(X i) в целевой алгебре.

LaTeX

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

Lean4

@[simp]
theorem commAlgEquiv_X (i) : commAlgEquiv R S₁ S₂ (.X i) = .C (.X i) := by simp [commAlgEquiv]

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

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

Разделы

Аффилиация

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