mathlib

0efabe73 - fix(geometry/euclidean/angle/unoriented/right_angle): fix lemma naming (#17941)

fix(geometry/euclidean/angle/unoriented/right_angle): fix lemma naming (#17941) As pointed out by @eric-wieser in review of #17683 for corresponding oriented angle lemmas, some lemma names refer to `norm` but should refer to `dist`.