Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.exists_extension_norm_eq

Modification history

2020-11-22 22:06

src/analysis/normed_space/hahn_banach.lean

refactor(analysis/normed_space/hahn_banach): use is_R_or_C instead of specific typeclass (#5009) …

Added real.exists_extension_norm_eq View on Github →