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(linear_algebra/symplectic_group): add definition of symplectic group #15513

Closed
wants to merge 24 commits into from
Closed

[Merged by Bors] - feat(linear_algebra/symplectic_group): add definition of symplectic group #15513

wants to merge 24 commits into from

Commits on Jul 14, 2022

  1. add symplectic group

    @mpenciak
    mpenciak committed Jul 14, 2022
    Configuration menu
    Copy the full SHA
    396d82f View commit details
    Browse the repository at this point in the history

  2. moving J

    @mcdoll
    mcdoll committed Jul 14, 2022
    Configuration menu
    Copy the full SHA
    d52bef0 View commit details
    Browse the repository at this point in the history

Commits on Jul 15, 2022

  1. changed imports and type order

    @mpenciak
    mpenciak committed Jul 15, 2022
    Configuration menu
    Copy the full SHA
    b266872 View commit details
    Browse the repository at this point in the history

  2. golf

    @mcdoll
    mcdoll committed Jul 15, 2022
    Configuration menu
    Copy the full SHA
    ed9aaf4 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2022

  1. trying to pass the linter (with TODOs)

    @mpenciak
    mpenciak committed Jul 16, 2022
    Configuration menu
    Copy the full SHA
    bba4120 View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2022

  1. back to one sorry

    @mcdoll
    mcdoll committed Jul 17, 2022
    Configuration menu
    Copy the full SHA
    26c1a74 View commit details
    Browse the repository at this point in the history

  2. no sorries

    @mcdoll
    mcdoll committed Jul 17, 2022
    Configuration menu
    Copy the full SHA
    7683336 View commit details
    Browse the repository at this point in the history

  3. removing old things

    @mcdoll
    mcdoll committed Jul 17, 2022
    Configuration menu
    Copy the full SHA
    182c625 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2022

  1. move symplectic_group to matrix namespace

    @mpenciak
    mpenciak committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    2e49327 View commit details
    Browse the repository at this point in the history

  2. delete coercion to fun

    @mpenciak
    mpenciak committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    c6891e9 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2022

  1. first part of removal of redundant units lemma

    @mcdoll
    mcdoll committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    b53a0b0 View commit details
    Browse the repository at this point in the history

  2. second part

    @mcdoll
    mcdoll committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    050b116 View commit details
    Browse the repository at this point in the history

  3. removed det lemma

    @mcdoll
    mcdoll committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    c66c305 View commit details
    Browse the repository at this point in the history

  4. remove unused assumption

    @mpenciak
    mpenciak committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    4b4045f View commit details
    Browse the repository at this point in the history

  5. added inv_eq_symplectic_inv

    @mpenciak
    mpenciak committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    b2e0728 View commit details
    Browse the repository at this point in the history

  6. another unused assumption

    @mpenciak
    mpenciak committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    ddf08ca View commit details
    Browse the repository at this point in the history

  7. add coe_inv'

    @mpenciak
    mpenciak committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    9c54bbb View commit details
    Browse the repository at this point in the history

  8. golfed (helped by mcdoll)

    @mpenciak
    mpenciak committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    dc6dfd3 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2022

  1. another golf

    @mcdoll
    mcdoll committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    047f1eb View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2022

  1. address reviewer comments

    @mpenciak
    mpenciak committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    de12d0f View commit details
    Browse the repository at this point in the history

  2. fix linter issues

    @mpenciak
    mpenciak committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    15aeda0 View commit details
    Browse the repository at this point in the history

Commits on Aug 30, 2022

  1. actually fixed linter issues

    @mpenciak
    mpenciak committed Aug 30, 2022
    Configuration menu
    Copy the full SHA
    5a2072b View commit details
    Browse the repository at this point in the history

Commits on Aug 31, 2022

  1. change coe_inv again

    @mpenciak
    mpenciak committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    edcee9a View commit details
    Browse the repository at this point in the history

Commits on Sep 5, 2022

  1. removed @[simp] for coe_inv and some golfs

    @mcdoll
    mcdoll committed Sep 5, 2022
    Configuration menu
    Copy the full SHA
    dcdd393 View commit details
    Browse the repository at this point in the history