mathlib3

8836a42d - fix(linear_algebra/quadratic_form/basic): align diamonds in the nat- and int- action (#12541)

fix(linear_algebra/quadratic_form/basic): align diamonds in the nat- and int- action (#12541) This also provides `fun_like` and `zero_hom_class` instances. The `has_scalar` code has been moved unchanged from further down in the file. This change makes `coe_fn_sub` eligible for `dsimp`, since it can now be proved by `rfl`.