New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(group_theory): subgroups of real numbers #4334
Conversation
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
lgtm, modulo trivial stuff
bors d+
@@ -889,6 +938,9 @@ begin | |||
refine ⟨-n, neg_gsmul x n⟩ } | |||
end | |||
|
|||
lemma closure_singleton_zero : closure ({0} : set A) = ⊥ := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess it can't be deduced from closure_singleton_one
through to_additive
? Even if it can't, it's good to register (after the fact) a to_additive
attribute so that later proofs can be converted automatically.
@@ -226,6 +229,9 @@ lemma mem_closure_singleton {x y : A} : | |||
y ∈ closure ({x} : set A) ↔ ∃ n:ℕ, n •ℕ x = y := | |||
by rw [closure_singleton_eq, add_monoid_hom.mem_mrange]; refl | |||
|
|||
lemma closure_singleton_zero : closure ({0} : set A) = ⊥ := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ditto
✌️ PatrickMassot can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
bors r+ |
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> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
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> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
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