Theorem closure_subset_mul_right_of_mem_nhds_one_of_inv

Modification history

2026-06-10 13:05
Mathlib/Topology/Algebra/Group/Pointwise.lean
feat(Topology/Algebra/Module/LocallyConvex): a very nice basis of locally convex spaces (#39063) …
Added closure_subset_mul_right_of_mem_nhds_one_of_invView on Github →