Commit 2022-09-21 08:15 a6d28ae9

View on Github →

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.

Estimated changes