Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-15 09:20 7e5be024

View on Github →

chore(algebra/*): make non-instance typeclasses reducible. (#8322) A follow up to #7835

Estimated changes

Modified src/algebra/algebra/basic.lean

Modified src/algebra/module/basic.lean

modified def module.comp_hom

Modified src/group_theory/group_action/defs.lean

modified def distrib_mul_action.comp_hom

modified def mul_action.comp_hom