mathlib
dccc5421 - fix(algebra/group/pi): remove unnecessary add_monoid requirement from pi.single_zero (#6325)

Commit
5 years ago
fix(algebra/group/pi): remove unnecessary add_monoid requirement from pi.single_zero (#6325) Follows on from #6317
Author
Parents
Loading