Theorem Rep.linearization_obj_ρ

Modification history

2025-06-04 06:26
Mathlib/RepresentationTheory/Rep.lean
feat(RepresentationTheory/*): `Rep.diagonal k G (n + 1) ≅ Rep.free k G (Fin n → G) ` (#21736) …
Modified Rep.linearization_obj_ρView on Github →
2025-02-25 19:33
Mathlib/RepresentationTheory/Rep.lean
refactor(CategoryTheory/Action/*): make `Action.rho` a `MonoidHom` instead of a morphism in `MonCat` (#21652)
Modified Rep.linearization_obj_ρView on Github →
2023-06-21 09:25
Mathlib/RepresentationTheory/Rep.lean
feat: port RepresentationTheory.Rep (#5041)
Added Rep.linearization_obj_ρView on Github →