Theorem: Section20Sheet2Solutions.RepMap.comp_assoc (FormalisingMathematics2024/Solutions/Section20representationTheory/Sheet2.lean)

State before:
k : Type
inst✝⁹ : Field k
G : Type
inst✝⁸ : Group G
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
W : Type
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝³ : AddCommGroup X
inst✝² : Module k X
τ : Representation k G X
Y : Type
inst✝¹ : AddCommGroup Y
inst✝ : Module k Y
υ : Representation k G Y
ξ : RepMap τ υ
ψ : RepMap σ τ
φ : RepMap ρ σ
⊢ comp (comp ξ ψ) φ = comp ξ (comp ψ φ)
Tactic:
rfl
State after:
no goals