mathlib

a6d28ae9 - feat(topology/algebra/mul_action): `add_torsor.connected_space` (#16471)

feat(topology/algebra/mul_action): `add_torsor.connected_space` (#16471) Add the lemma that an `add_torsor` for a connected space is itself a connected space, given `has_continuous_vadd`.