linHom_apply

Mathlib.RepresentationTheory.Basic

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

English

The simp-annotated lemma states that (linHom ρV ρW) g f equals ρW g ∘ f ∘ ρV g^{-1} for the given g and f.

Русский

Лемма с пометкой simp говорит, что (linHom ρV ρW) g f = ρW g ∘ f ∘ ρV g^{-1}.

LaTeX

$$$ (linHom ρ_V ρ_W) g f = ρ_W g \\circ f \\circ ρ_V g^{-1} $$$

Lean4

@[simp]
theorem linHom_apply (g : G) (f : V →ₗ[k] W) : (linHom ρV ρW) g f = ρW g ∘ₗ f ∘ₗ ρV g⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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