mathlib

8412f1fc - feat(representation_theory/invariants): invariants of `lin_hom` are representation morphisms (#14012)