mathlib
c88e8f35 - refactor(*): drop `topology/instances/complex` (#5208)

Commit
5 years ago
refactor(*): drop `topology/instances/complex` (#5208) * drop `topology/instances/complex`, deduce topology from `normed_space` instead; * generalize continuity of `polynomial.eval` to any `topological_ring`; add versions for `evalâ‚‚` and `aeval`; * replace `polynomial.tendsto_infinity` with `tendsto_abv_at_top`, add versions for `evalâ‚‚`, `aeval`, as well as `norm` instead of `abv`. * generalize `complex.exists_forall_abs_polynomial_eval_le` to any `[normed_ring R] [proper_space R]` such that norm is multiplicative, rename to `polynomial.exists_forall_norm_le`.
Author
Parents
Loading