mathlib3

16d04da2 - `injective.group_div` ensures the division is defeq to the existing `has_div` instance