Commit 2021-12-09 08:54 70171ac4

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.