domDomCongr_tprod

Mathlib.LinearAlgebra.TensorPower.Symmetric

URI: https://scilib.ai/kg/mathlib#SymmetricPower.domDomCongr_tprod

English

In symmetric powers, a permutation yields the same tprod under domDomCongr.

Русский

В симметрических степенях перестановка приводит к той же tprod под domDomCongr.

LaTeX

$$theorem: domDomCongr_tprod for SymmetricPower$$

Lean4

@[simp]
theorem domDomCongr_tprod (e : Perm ι) : (tprod R (ι := ι) (M := M)).domDomCongr e = tprod R :=
  MultilinearMap.ext <| tprod_equiv e

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

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

Разделы

Аффилиация

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