Topological affine spaces

Stream: maths

[Yury G. Kudryashov]

I'm adding topological_add_torsors in #13412. My main motivation is to be able to prove, e.g., continuity of docs#affine_map.line_map simultaneously for topological additive groups and for normed add torsors. I get some strange elaboration issues down the road. Usually, they can be solved by using convert but I fail to understand why they happen.