algebra) : giving `C(α, M)` a `has_continuous_mul` and a `has_continuous_smul` structure (#11261)

Commit

3 years ago

feat(topology/continuous/algebra) : giving `C(α, M)` a `has_continuous_mul` and a `has_continuous_smul` structure (#11261) Here, `α` is a locally compact space. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

laughinggas

Parents

77110125

mathlib3 b7d6b3aa - feat(topology/continuous/algebra) : giving `C(α, M)` a `has_continuous_mul` and a `has_continuous_smul` structure (#11261)

mathlib3
b7d6b3aa - feat(topology/continuous/algebra) : giving `C(α, M)` a `has_continuous_mul` and a `has_continuous_smul` structure (#11261)