Mathlib v3 is deprecated. Go to Mathlib v4

Theorem weak_dual.to_normed_dual_apply

Modification history

2022-06-01 09:18
src/analysis/normed_space/weak_dual.lean
feat(analysis/normed_space/star/character_space): compactness of the character space of a normed algebra (#14135) …
Added weak_dual.to_normed_dual_applyView on Github →