Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.tendsto_cocompact_mul_left₀

Modification history

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