tensor_ρ — Mathlib

English

For representations A,B of G, the action on the tensor product is the tensor product of the actions: (A ⊗ B).ρ(g) = A.ρ(g) ⊗ B.ρ(g) for all g ∈ G.

Русский

Для представлений A и B of G верно, что действие на тензорном произведении равно тензорному произведению действий: (A ⊗ B).ρ(g) = A.ρ(g) ⊗ B.ρ(g) для всех g ∈ G.

LaTeX

$$$(A \\otimes B).\\rho(g) = A.\\rho(g) \\otimes B.\\rho(g)\\quad(\\text{для всех } g\\in G)$$$

Lean4

@[simp]
theorem tensor_ρ {A B : Rep k G} : (A ⊗ B).ρ = A.ρ.tprod B.ρ :=
  rfl

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