Theorem Rep.res_map_hom_toLinearMap

Modification history

2026-06-30 17:51

Mathlib/RepresentationTheory/Rep/Res.lean

refactor(RepresentationTheory/Rep/Res): refactor resFunctor (#41054) …

Deleted Rep.res_map_hom_toLinearMap View on Github →

2026-03-24 21:13

Mathlib/RepresentationTheory/Rep/Res.lean

chore(RepresentationTheory): Refactor Rep (#36127) …

Added Rep.res_map_hom_toLinearMap View on Github →