mathlib3

26fcfbc9 - feat(topology): continuous_pi_iff pi.has_continuous_mul pi.topological_group (#6689)