algebraTensorAlgEquiv_symm_X

Mathlib.RingTheory.TensorProduct.MvPolynomial

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

English

The inverse of algebraTensorAlgEquiv sends the polynomial variable X_s to 1 ⊗ X_s.

Русский

Обратное к algebraTensorAlgEquiv отправляет переменную X_s в 1 ⊗ X_s.

LaTeX

$$$ (algebraTensorAlgEquiv(R,A)).symm(X_s) = 1 \\otimes_{} X_s $$$

Lean4

@[simp]
theorem algebraTensorAlgEquiv_symm_X (s : σ) : (algebraTensorAlgEquiv R A).symm (X s) = 1 ⊗ₜ X s := by
  simp [algebraTensorAlgEquiv]

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

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

Разделы

Аффилиация

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