mathlib3

27c86764 - refactor(geometry/manifold/algebra/smooth_functions): make `smooth_map_group` division defeq to `pi.has_div` (#6912)

refactor(geometry/manifold/algebra/smooth_functions): make `smooth_map_group` division defeq to `pi.has_div` (#6912) The motivation was the fact that this allows `smooth_map.coe_div` to be `rfl` but this should be more generally useful.