Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Module.monoidal_category.tensor_id

Modification history

2022-07-07 00:12
src/algebra/category/Module/monoidal.lean
refactor(group_theory/congruence): use `quotient.map` (#15130) …
Modified Module.monoidal_category.tensor_idView on Github →
2020-03-14 08:02
src/algebra/category/Module/monoidal.lean
feat(algebra): monoidal category of R-modules (#2125) …
Added Module.monoidal_category.tensor_idView on Github →