mathlib3

feat(algebra/group/units): add some lemmas about `divp`

#1388

Merged