mathlib3

0bc7c2d5 - fix(algebra/group/{prod,pi}): fix non-defeq `has_scalar` diamonds (#9584)

fix(algebra/group/{prod,pi}): fix non-defeq `has_scalar` diamonds (#9584) This fixes diamonds in the following instances for nat- and int- actions: * `has_scalar ℕ (α × β)` * `has_scalar ℤ (α × β)` * `has_scalar ℤ (Π a, β a)` The last one revealed a diamond caused by inconsistent use of `pi_instance_derive_field`: ```lean -- fails before this change example [Π a, group $ β a] : group.to_div_inv_monoid (Π a, β a) = pi.div_inv_monoid := rfl ```