Commit 2025-03-31 13:41 f6d75be5

View on Github →

feat: orbits of an irrational rotation are dense (#16596)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/Order/Archimedean.lean

deleted theorem AddSubgroup.dense_of_no_min

deleted theorem AddSubgroup.dense_of_not_isolated_zero

deleted theorem AddSubgroup.dense_or_cyclic

added theorem Subgroup.dense_iff_ne_zpowers

added theorem Subgroup.dense_of_no_min

added theorem Subgroup.dense_of_not_isolated_one

added theorem Subgroup.dense_or_cyclic

added theorem Subgroup.dense_xor'_cyclic

Modified Mathlib/Topology/Algebra/Order/Group.lean

Modified Mathlib/Topology/Instances/AddCircle.lean

added theorem AddCircle.addOrderOf_coe_eq_zero_iff_forall_rat_ne_div

added theorem AddCircle.finite_setOf_addOrderOf_eq

deleted theorem AddCircle.finite_setOf_add_order_eq

Created Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean

added theorem AddCircle.denseRange_zsmul_coe_iff

added theorem AddCircle.denseRange_zsmul_iff

added theorem AddCircle.dense_addSubgroup_iff_ne_zmultiples

added theorem dense_addSubgroupClosure_pair_iff