mathlib3

ba169870 - chore(*): Remove definitions which now exist elsewhere

chore(*): Remove definitions which now exist elsewhere For the sake of review, this leaves the definitions behind as aliases. They will be removed in a later commit