Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-30 14:01 a1927830

View on Github →

chore(algebra/direct_sum_graded): relax typeclass assumptions (#6961)

Estimated changes

Modified src/algebra/direct_sum_graded.lean

modified def direct_sum.ghas_mul.of_add_subgroups

modified def direct_sum.ghas_mul.of_add_submonoids

modified def direct_sum.ghas_mul.to_sigma_has_mul

modified def direct_sum.ghas_one.of_add_subgroups

modified def direct_sum.ghas_one.of_add_submonoids