Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-01 20:40 4ef680b1

View on Github →

feat(group_theory): subgroups of real numbers (#4334) This fills the last hole in the "Topology of R" section of our undergrad curriculum: additive subgroups of real numbers are either dense or cyclic. Most of this PR is supporting material about ordered abelian groups. Co-Authored-By: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com

Estimated changes

added theorem gsmul_nonneg
added theorem nsmul_lt_nsmul
modified theorem nsmul_nonneg
added theorem nsmul_pos
added theorem gsmul_le_gsmul
added theorem gsmul_le_gsmul_iff
added theorem gsmul_lt_gsmul
added theorem gsmul_lt_gsmul_iff
added theorem gsmul_pos
added theorem nsmul_le_nsmul_iff
added theorem nsmul_lt_nsmul_iff
added theorem int.subgroup_cyclic
added theorem real.mem_closure_iff