Commit 2022-03-10 06:34 8836a42d

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.