mathlib3

7a485b1b - feat(topology/continuous_function/algebra): `C(α, β)` is a topological group (#11665)

feat(topology/continuous_function/algebra): `C(α, β)` is a topological group (#11665) This PR proves that `C(α, β)` is a topological group. I had to borrow the fix from #11229 to avoid a diamond.