Mathlib v3 is deprecated. Go to Mathlib v4

Def inner_product_space.to_dual

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) …
Modified inner_product_space.to_dualView on Github →
2021-10-06 08:03
src/analysis/inner_product_space/dual.lean
refactor(analysis/{normed_space, inner_product_space}/dual): redefine using `linear_isometry` (#9569) …
Modified inner_product_space.to_dualView on Github →
2021-09-30 02:06
src/analysis/inner_product_space/dual.lean
refactor(analysis/normed_space/{dual, pi_Lp}): split out inner product space parts (#9388) …
Modified inner_product_space.to_dualView on Github →
2020-11-28 16:26
src/analysis/normed_space/dual.lean
feat(analysis/normed_space/dual): Fréchet-Riesz representation for the dual of a Hilbert space (#4379) …
Added inner_product_space.to_dualView on Github →