Theorem closure_subset_of_mem_nhds_one_of_inv_mul_right_subset

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_of_mem_nhds_one_of_inv_mul_right_subsetView on Github →