repOfTprodIso_inv_apply

Mathlib.RepresentationTheory.Rep

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

English

The inverse repOfTprodIso also acts as identity on tensors.

Русский

Обратное repOfTprodIso также действует как тождество на тензоре.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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