Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-02 17:29 3913d303

View on Github →

refactor(topology/algebra): use dot notation in tendsto.add and friends (#1765)

Estimated changes

Modified src/analysis/calculus/fderiv.lean

Modified src/analysis/calculus/tangent_cone.lean

Modified src/analysis/complex/exponential.lean

Modified src/analysis/normed_space/banach.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/analysis/normed_space/real_inner_product.lean

Modified src/analysis/specific_limits.lean

Modified src/data/padics/hensel.lean

Modified src/data/real/hyperreal.lean

Modified src/measure_theory/decomposition.lean

Modified src/topology/algebra/group.lean

added theorem filter.tendsto.inv

added theorem filter.tendsto.sub

deleted theorem tendsto.inv

deleted theorem tendsto.sub

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/monoid.lean

added theorem filter.tendsto.mul

deleted theorem tendsto.mul

Modified src/topology/algebra/uniform_group.lean

Modified src/topology/instances/nnreal.lean

Modified src/topology/instances/real.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean