Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 07:59 1e72fb3f

View on Github →

feat(representation_theory/Action): mapping by a monoidal functor (#14331)

Estimated changes

Modified src/representation_theory/Action.lean

added theorem Action.tensor_unit_V

added theorem Action.tensor_unit_rho

added def category_theory.monoidal_functor.map_Action