mathlib3

70171ac4 - feat(topology/instances/real_vector_space): add an `is_scalar_tower` instance (#10490)

feat(topology/instances/real_vector_space): add an `is_scalar_tower` instance (#10490) There is at most one topological real vector space structure on a topological additive group, so `[is_scalar_tower real A E]` holds automatically as long as `A` is a topological real algebra and `E` is a topological module over `A`.