Commit 2020-11-22 22:06 17a6f6da

refactor(analysis/normed_space/hahn_banach): use is_R_or_C instead of specific typeclass (#5009) In the current version, the proof of Hahn-Banach theorem is given over the reals, then over the complexes, and then to state the consequences uniformly a custom typeclass is defined. The proof over the complexes in fact works directly over any is_R_or_C field (i.e., reals or complexes), so we reformulate the proof in these terms, avoiding the custom typeclass. It doesn't bring any new theorem to mathlib, but it may be helpful in the future (to prove results uniformly over reals and complexes using is_R_or_C) if we have Hahn-Banach readily available for this typeclass.