mathlib3
14cff9ac - chore(algebra/group/pi): add `pi.has_div` (#4776)

Commit
5 years ago
chore(algebra/group/pi): add `pi.has_div` (#4776) Motivated by #4646
Author
Parents
Loading