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`.





leanprover-community/mathlib,leanprover-community/mathlib