Commit 2020-07-14 11:42 0fff477d

View on Github →

feat(analysis/normed_space): complex Hahn-Banach theorem (#3286) This proves the complex Hahn-Banach theorem by reducing it to the real version. The corollaries from #3021 should be generalized as well at some point.

Estimated changes

Created src/analysis/normed_space/extend.lean

added theorem norm_bound

Modified src/analysis/normed_space/hahn_banach.lean

added theorem complex.exists_extension_norm_eq

Modified src/data/complex/basic.lean

added theorem complex.I_mul

added theorem complex.abs_ne_zero

added theorem complex.of_real_smul