Commit 2025-02-27 22:45 da2b5ec4

View on Github →

refactor(RepresentationTheory/Rep): golf some proofs (#22338)

Estimated changes

Modified Mathlib/CategoryTheory/Action/Monoidal.lean

added theorem Action.β_hom_hom

added theorem Action.β_inv_hom

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RepresentationTheory/Rep.lean

deleted theorem Rep.MonoidalCategory.braiding_hom_apply

deleted theorem Rep.MonoidalCategory.braiding_inv_apply

added def Rep.leftRegularHom

deleted theorem Rep.leftRegularHom_apply

added theorem Rep.leftRegularHom_hom_single

added theorem Rep.tensor_ρ