basic): completion of an `inner_product_space` is an `inner_product_space` (#16407)

Commit

3 years ago

feat(analysis/inner_product_space/basic): completion of an `inner_product_space` is an `inner_product_space` (#16407)

Author

ADedecker

Parents