uniform_group): `cauchy_seq.const_mul` and friends (#11917)

Commit

3 years ago

feat(topology/algebra/uniform_group): `cauchy_seq.const_mul` and friends (#11917) A Cauchy sequence multiplied by a constant (including `-1`) remains a Cauchy sequence.

Author

ecstatic-morse

Parents

4545e31e

mathlib a3d6b43c - feat(topology/algebra/uniform_group): `cauchy_seq.const_mul` and friends (#11917)

mathlib
a3d6b43c - feat(topology/algebra/uniform_group): `cauchy_seq.const_mul` and friends (#11917)