Theorem inner_product_space.to_dual'_isometry
Modification history
2021-10-28 09:24
src/analysis/inner_product_space/dual.lean
feat(analysis/inner_product_space/dual): complex Riesz representation theorem (#9924) …
Deleted inner_product_space.to_dual'_isometryView on Github →