Commit 2026-02-24 17:56 681dd0c2

feat: definition of equivalence of representations (#34888) Defines equivalence of representations, and defines an equivalence between $$\mathrm{Hom}(V, W)$$ and $$V^* \otimes W$$ as representations. This is a missing piece to respell all of the results in Character.lean without using category-theoretic notions.