Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-14 12:41 a998fd10

View on Github →

feat(algebra/category/Module): the monoidal category of R-modules is symmetric (#4140)

Estimated changes

Modified src/algebra/category/Module/monoidal.lean

added def Module.braiding

added theorem Module.braiding_naturality

added theorem Module.hexagon_forward

added theorem Module.hexagon_reverse

added theorem Module.monoidal_category.braiding_hom_apply

added theorem Module.monoidal_category.braiding_inv_apply