Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_subgroup.tendsto_zmultiples_subtype_cofinite

Modification history

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