dual): remove unneeded `complete_space` assumption in four lemmas (#11578)

Commit

4 years ago

chore(analysis/inner_product_space/dual): remove unneeded `complete_space` assumption in four lemmas (#11578) We remove the `[complete_space E]` assumption in four lemmas.

Author

dupuisf

Parents

80e072ec

mathlib3 884d8137 - chore(analysis/inner_product_space/dual): remove unneeded `complete_space` assumption in four lemmas (#11578)

mathlib3
884d8137 - chore(analysis/inner_product_space/dual): remove unneeded `complete_space` assumption in four lemmas (#11578)