mathlib3
2bb1bae8 - chore(analysis/locally_convex/[continuous_of_]bounded): import `analysis.normed_space.is_R_or_C` later (#16758)

Commit
3 years ago
chore(analysis/locally_convex/[continuous_of_]bounded): import `analysis.normed_space.is_R_or_C` later (#16758) We don't want to import `analysis/normed_space/is_R_or_C` in `analysis/locally_convex/bounded` because it will create a cycle when defining the strong topology on `continuous_linear_map`, because we will have to (transitively) import `analysis/locally_convex/bounded` in `analysis/normed_space/operator_norm`. So I moved the material of #16550 in a new file `analysis/locally_convex/continuous_of_bounded`
Author
Parents
Loading