mathlib3

7ec8f8a2 - feat(analysis/inner_product_space/basic): `ext_inner_map` (#16388)

feat(analysis/inner_product_space/basic): `ext_inner_map` (#16388) Equality of operators by equality of inner products. An easy corollary of `inner_map_self_eq_zero`.