Commit 2026-06-30 17:51 7d6ecd37
View on Github →refactor(RepresentationTheory/Rep/Res): refactor resFunctor (#41054)
This PR refactors the definition of resFunctor, in the current master since the whole definition is an abbrev, everything is exposed and if one does ext; simp one of the possible outcome in the infoview would be
ofHom { toLinearMap := (Hom.hom ..).toLinearMap, isIntertwining' := ⋯ }
which is not helpful unfolds too much, this PR seals the map part of the functor to make it less transparent while keep the definition of resFunctor as an abbrev to maintain the full transparency on the underlying type.