mathlib

a81201cc - feat(topology/algebra): add converse to tendsto.mul (#18276)

feat(topology/algebra): add converse to tendsto.mul (#18276) In a topological group-with-zero, if`f * g` tends to `x * y` and `g` tends to `y`, with `y \ne 0`, then `f` tends to `x`.