Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-06 11:43 c88e8f35

View on Github →

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.

Estimated changes