mathlib

30cfcc45 - move to eq_to_hom, rename