English
Let ρ be a representation of G on a finite-dimensional vector space V. The construction of the FDRep object from ρ preserves the original action map, i.e., the ρ component of the new representation equals ρ.
Русский
Пусть ρ – представление группы G на конечномерном пространстве V. Конструкция FDRep, созданная из ρ, сохраняет исходное отображение действия: компоненту ρ новой репрезентации можно восстановить как ρ.
LaTeX
$$$(FDRep.of\ ρ).ρ = ρ$$$
Lean4
/-- This lemma is about `FDRep.ρ`, instead of `Action.ρ` for `of_ρ`. -/
@[simp]
theorem of_ρ' {V : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] (ρ : G →* V →ₗ[R] V) : (of ρ).ρ = ρ :=
rfl
