Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-27 11:53 72944168

View on Github →

feat(topology/instances/real): classify discrete subgroups (#16592) The subgroups aℤ (i.e. zmultiples a) of ℝ are discrete, in the sense of having finite intersection with any compact subset.

Estimated changes

Modified src/group_theory/subgroup/basic.lean

added theorem monoid_hom.coe_comp_range_restrict

added theorem monoid_hom.subtype_comp_range_restrict

Modified src/topology/algebra/field.lean

added theorem filter.tendsto_cocompact_mul_left₀

added theorem filter.tendsto_cocompact_mul_right₀

Modified src/topology/algebra/monoid.lean

added theorem filter.tendsto_cocompact_mul_left

added theorem filter.tendsto_cocompact_mul_right

Modified src/topology/instances/real.lean

added theorem add_subgroup.tendsto_zmultiples_subtype_cofinite

added theorem int.tendsto_coe_cofinite

added theorem int.tendsto_zmultiples_hom_cofinite

Modified src/topology/metric_space/basic.lean

deleted theorem int.tendsto_coe_cofinite