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

refactor(group_theory/abelianization): simplify abelianization #1126

Merged
merged 16 commits into from
Jun 11, 2019
Merged

refactor(group_theory/abelianization): simplify abelianization #1126

merged 16 commits into from
Jun 11, 2019

Commits on May 15, 2019

  1. feat(group_theory/conjugates) : define conjugates 

    define group conjugates and normal closure
    Michael Howes committed May 15, 2019
    Configuration menu
    Copy the full SHA
    c423f8d View commit details
    Browse the repository at this point in the history

  2. feat(algebra/order_functions): generalize strict_mono.monotone (#1022)

    @rwbarton
    rwbarton authored and Michael Howes committed May 15, 2019
    Configuration menu
    Copy the full SHA
    d907045 View commit details
    Browse the repository at this point in the history

  3. trying to merge

    Michael Howes committed May 15, 2019
    Configuration menu
    Copy the full SHA
    4287c1b View commit details
    Browse the repository at this point in the history

  4. fixing merge

    Michael Howes committed May 15, 2019
    Configuration menu
    Copy the full SHA
    e15ab8f View commit details
    Browse the repository at this point in the history

Commits on Jun 7, 2019

  1. feat(group_theory\presented_group): define presented groups 

    Presented groups are defined as a quotient of a free group by the normal subgroup  the relations generate.
    Michael Howes committed Jun 7, 2019
    Configuration menu
    Copy the full SHA
    af1d318 View commit details
    Browse the repository at this point in the history

  2. feat(group_theory\presented_group): define presented groups 

    Presented groups are defined as a quotient of a free group by the normal subgroup  the relations generate
    Michael Howes committed Jun 7, 2019
    Configuration menu
    Copy the full SHA
    312a61d View commit details
    Browse the repository at this point in the history

  3. Update src/group_theory/presented_group.lean 

    Co-Authored-By: Keeley Hoek <keeley@hoek.io>
    @Michael-Howes @khoek
    Michael-Howes and khoek committed Jun 7, 2019
    Configuration menu
    Copy the full SHA
    f910fa5 View commit details
    Browse the repository at this point in the history

Commits on Jun 8, 2019

  1. Merge remote-tracking branch 'upstream/master'

    Michael Howes committed Jun 8, 2019
    Configuration menu
    Copy the full SHA
    b04f47c View commit details
    Browse the repository at this point in the history

  2. Uniqueness of extension

    Michael Howes committed Jun 8, 2019
    Configuration menu
    Copy the full SHA
    415cd51 View commit details
    Browse the repository at this point in the history

  3. Tidied up to_group.unique

    Michael Howes committed Jun 8, 2019
    Configuration menu
    Copy the full SHA
    69fa4a0 View commit details
    Browse the repository at this point in the history

  4. Removed unnecessary line

    Michael Howes committed Jun 8, 2019
    Configuration menu
    Copy the full SHA
    3419830 View commit details
    Browse the repository at this point in the history

  5. Changed naming

    Michael Howes committed Jun 8, 2019
    Configuration menu
    Copy the full SHA
    75d85c9 View commit details
    Browse the repository at this point in the history

Commits on Jun 10, 2019

  1. Merge branch 'master' into master

    @mergify
    mergify[bot] committed Jun 10, 2019
    Configuration menu
    Copy the full SHA
    b3ffb69 View commit details
    Browse the repository at this point in the history

  2. Merged with upstream

    Michael Howes committed Jun 10, 2019
    Configuration menu
    Copy the full SHA
    a69d654 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' of https://github.com/Michael-Howes/mathlib

    Michael Howes committed Jun 10, 2019
    Configuration menu
    Copy the full SHA
    2d415f5 View commit details
    Browse the repository at this point in the history

  4. refactor(group_theory/abelianization): simplify abelianization 

    The commutator of a group was previously defined using lists.
Now it is defined using `normal_closure`.
This change simplifies some of the proofs
    Michael Howes committed Jun 10, 2019
    Configuration menu
    Copy the full SHA
    c1e7c71 View commit details
    Browse the repository at this point in the history