Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.tendsto_cocompact_mul_left

Modification history

2022-09-27 11:53
src/topology/algebra/monoid.lean
feat(topology/instances/real): classify discrete subgroups (#16592) …
Added filter.tendsto_cocompact_mul_leftView on Github →