Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-01 12:31 f2c84aa0

View on Github →

doc(algebra/category/*): provide two short docstrings and shorten lines (#5984) also fixed one minor typo.

Estimated changes

Modified src/algebra/category/Algebra/basic.lean

Modified src/algebra/category/CommRing/colimits.lean

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

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

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

modified def Module.monoidal_category.tensor_hom

Modified src/algebra/category/Mon/colimits.lean

modified theorem Mon.colimits.quot_mul