Commit 2021-10-17 13:18 1432c308

feat(topology/algebra/mul_action): λ x, c • x is a closed map for all c (#9756)

• rename old is_closed_map_smul₀ to is_closed_map_smul_of_ne_zero;
• add a new is_closed_map_smul₀ that assumes more about typeclasses but works for c = 0.