mathlib3

22131150 - feat(topology/uniform_space/cauchy): `mul_opposite X` is complete when `X` is (#18471)

feat(topology/uniform_space/cauchy): `mul_opposite X` is complete when `X` is (#18471) The new import is needed because the lemmas about the topology on `mul_opposite` aren't available yet, even though the instance itself is (via the uniformity instance). Forward-ported as https://github.com/leanprover-community/mathlib4/pull/2404.