dual,adjoint): add some lemmas about extensionality with respect to a basis (#11176)

Commit

3 years ago

feat(analysis/inner_product_space/dual,adjoint): add some lemmas about extensionality with respect to a basis (#11176) This PR adds some lemmas about extensionality in inner product spaces with respect to a basis.

Author

dupuisf

Parents

03872fdd

mathlib3 1aec9a19 - feat(analysis/inner_product_space/dual,adjoint): add some lemmas about extensionality with respect to a basis (#11176)

mathlib3
1aec9a19 - feat(analysis/inner_product_space/dual,adjoint): add some lemmas about extensionality with respect to a basis (#11176)