mathlib3

8ba7df83 - feat(topology/algebra/algebra): ℚ-scalar multiplication is continuous (#13458)