mathlib3

9a517cf0 - chore(analysis/normed/group/completion): fix attribution (#11614)

chore(analysis/normed/group/completion): fix attribution (#11614) This code was written by @jcommelin in #6189 but somehow acquired my name during a refactor (#10055). I don't think I've ever touched it!