Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-26 13:30 c5a8a818

View on Github →

refactor(topology/algebra/uniform_group): Use to_additive. (#11662) This PR refactors topology/algebra/uniform_group to use to_additive.

Estimated changes

deleted theorem cauchy_seq.add
added theorem cauchy_seq.mul
modified theorem group_separation_rel
added theorem tendsto_div_comap_self
deleted theorem tendsto_sub_comap_self
deleted theorem to_uniform_space_eq
deleted theorem uniform_add_group.mk'
deleted theorem uniform_continuous.add
added theorem uniform_continuous.div
added theorem uniform_continuous.inv
added theorem uniform_continuous.mul
deleted theorem uniform_continuous.neg
deleted theorem uniform_continuous.sub
deleted theorem uniform_continuous_add
added theorem uniform_continuous_div
added theorem uniform_continuous_inv
added theorem uniform_continuous_mul
deleted theorem uniform_continuous_neg
deleted theorem uniform_continuous_sub
added theorem uniform_group.mk'
deleted theorem uniformity_translate