mathlib3

5809296d - doc(analysis/normed/group/basic): add docstring explaining the "insert" name