mathlib3

020c8755 - moved homogeneous_core upfront, changed definition