mathlib

fd51bda5 - feat(analysis/normed_space/linear_isometry): basis ext lemmas (#11331)

feat(analysis/normed_space/linear_isometry): basis ext lemmas (#11331) Add lemmas that two linear isometries / linear isometric equivalences are equal if they are equal on basis vectors, similar to such lemmas for equality on basis vectors of other kinds of maps.