repOfTprodIso_apply

Mathlib.RepresentationTheory.Rep

URI: https://scilib.ai/kg/mathlib#Representation.repOfTprodIso_apply

English

On the tensor V ⊗ W, repOfTprodIso acts as the identity map.

Русский

На тензоре V ⊗ W repOfTprodIso действует как тождественный отображатель.

LaTeX

$$$$ (repOfTprodIso \\; \\rho \\; \\tau).hom.hom x = x $$$$

Lean4

theorem repOfTprodIso_apply (x : TensorProduct k V W) : (repOfTprodIso ρ τ).hom.hom x = x :=
  rfl

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

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

Разделы

Аффилиация

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