Theorem: Section20sheet2.RepMap.comp_id (FormalisingMathematics2024/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
φ : RepMap ρ σ
⊢ comp φ (id ρ) = φ
Tactic:
sorry
State after:
no goals