Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(group_theory): subgroups of real numbers #4334

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat(group_theory): subgroups of real numbers #4334

wants to merge 19 commits into from

Commits on Sep 27, 2020

  1. WIP subgroups of reals

    @PatrickMassot
    PatrickMassot committed Sep 27, 2020
    Copy the full SHA
    80f3129 View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2020

  1. easy sorries

    @hrmacbeth
    hrmacbeth committed Sep 28, 2020
    Copy the full SHA
    c429f86 View commit details
    Browse the repository at this point in the history

  2. finish?

    @hrmacbeth
    hrmacbeth committed Sep 28, 2020
    Copy the full SHA
    e85d915 View commit details
    Browse the repository at this point in the history

  3. Cleanup

    @PatrickMassot
    PatrickMassot committed Sep 28, 2020
    Copy the full SHA
    b923877 View commit details
    Browse the repository at this point in the history

  4. Generalize inf_property

    @PatrickMassot
    PatrickMassot committed Sep 28, 2020
    Copy the full SHA
    5339536 View commit details
    Browse the repository at this point in the history

  5. wip

    @PatrickMassot
    PatrickMassot committed Sep 28, 2020
    Copy the full SHA
    e95ca61 View commit details
    Browse the repository at this point in the history

  6. Fix arguments order

    @PatrickMassot
    PatrickMassot committed Sep 28, 2020
    Copy the full SHA
    ff79428 View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2020

  1. two subgroup lemmas

    @hrmacbeth
    hrmacbeth committed Sep 29, 2020
    Copy the full SHA
    8cfb73b View commit details
    Browse the repository at this point in the history

  2. Reformulate in terms of add_subgroup.closure.

    @PatrickMassot
    PatrickMassot committed Sep 29, 2020
    Copy the full SHA
    72f2d20 View commit details
    Browse the repository at this point in the history

  3. duplicate subgroup theory to submonoid

    @hrmacbeth
    hrmacbeth committed Sep 29, 2020
    Copy the full SHA
    eefe688 View commit details
    Browse the repository at this point in the history

Commits on Sep 30, 2020

  1. extract lemma re: subgroups in archimedean groups

    @hrmacbeth
    hrmacbeth committed Sep 30, 2020
    Copy the full SHA
    1503137 View commit details
    Browse the repository at this point in the history

  2. linter

    @hrmacbeth
    hrmacbeth committed Sep 30, 2020
    Copy the full SHA
    6bbc273 View commit details
    Browse the repository at this point in the history

  3. consistency

    @hrmacbeth
    hrmacbeth committed Sep 30, 2020
    Copy the full SHA
    286c258 View commit details
    Browse the repository at this point in the history

  4. Some more lemmas

    @PatrickMassot
    PatrickMassot committed Sep 30, 2020
    Copy the full SHA
    d7e0b5b View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into subgroup_real

    @hrmacbeth
    hrmacbeth committed Sep 30, 2020
    Copy the full SHA
    0f8e6f6 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2020

  1. docs, naming, namespacing

    @hrmacbeth
    hrmacbeth committed Oct 1, 2020
    Copy the full SHA
    4b87b79 View commit details
    Browse the repository at this point in the history

  2. update undergrad.yaml

    @hrmacbeth
    hrmacbeth committed Oct 1, 2020
    Copy the full SHA
    c1584df View commit details
    Browse the repository at this point in the history

  3. Apply suggestions from code review 

    Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
    @hrmacbeth @robertylewis
    hrmacbeth and robertylewis committed Oct 1, 2020
    Copy the full SHA
    5213b1f View commit details
    Browse the repository at this point in the history

  4. Apply suggestions from code review 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @hrmacbeth @sgouezel
    hrmacbeth and sgouezel committed Oct 1, 2020
    Copy the full SHA
    14d60c6 View commit details
    Browse the repository at this point in the history