Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-07 00:12 e335a41f

View on Github →

refactor(group_theory/congruence): use quotient.map (#15130) Also add explicit universe levels in algebra.category.Module.monoidal.

Estimated changes

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

modified def Module.monoidal_category.associator

modified theorem Module.monoidal_category.tensor_id

Modified src/group_theory/congruence.lean

Modified src/group_theory/quotient_group.lean