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/orientation): composing with linear equivs and determinant #10737

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat(linear_algebra/orientation): composing with linear equivs and determinant #10737

wants to merge 15 commits into from

Commits on Dec 12, 2021

  1. feat(linear_algebra/orientation): composing with linear equivs and de… 

    …terminant

Add lemmas that composing an alternating map with a linear equiv using
`comp_linear_map`, or composing a basis with a linear equiv using
`basis.map`, produces the same orientation if and only if the
determinant of that linear equiv is positive.
    @jsm28
    jsm28 committed Dec 12, 2021
    Configuration menu
    Copy the full SHA
    26d5343 View commit details
    Browse the repository at this point in the history

  2. Add eq_neg_iff_det_neg lemmas.

    @jsm28
    jsm28 committed Dec 12, 2021
    Configuration menu
    Copy the full SHA
    7c54504 View commit details
    Browse the repository at this point in the history

  3. Fix long line, unneeded type class assumption.

    @jsm28
    jsm28 committed Dec 12, 2021
    Configuration menu
    Copy the full SHA
    7a54af4 View commit details
    Browse the repository at this point in the history

Commits on Dec 13, 2021

  1. Merge remote-tracking branch 'origin/master' into jsm28/orientation_c… 

    …omp_linear_equiv
    @jsm28
    jsm28 committed Dec 13, 2021
    Configuration menu
    Copy the full SHA
    2720c9f View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into jsm28/orientation_c… 

    …omp_linear_equiv
    @jsm28
    jsm28 committed Dec 13, 2021
    Configuration menu
    Copy the full SHA
    137932d View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into jsm28/orientation_c… 

    …omp_linear_equiv
    @jsm28
    jsm28 committed Dec 13, 2021
    Configuration menu
    Copy the full SHA
    092ce81 View commit details
    Browse the repository at this point in the history

Commits on Dec 14, 2021

  1. Merge remote-tracking branch 'origin/master' into jsm28/orientation_c… 

    …omp_linear_equiv
    @jsm28
    jsm28 committed Dec 14, 2021
    Configuration menu
    Copy the full SHA
    3ee3b0d View commit details
    Browse the repository at this point in the history

Commits on Dec 15, 2021

  1. chore(*): generalize lemmas

    @eric-wieser
    eric-wieser committed Dec 15, 2021
    Configuration menu
    Copy the full SHA
    afb759f View commit details
    Browse the repository at this point in the history

  2. fix namespacing

    @eric-wieser
    eric-wieser committed Dec 15, 2021
    Configuration menu
    Copy the full SHA
    c8bb6b3 View commit details
    Browse the repository at this point in the history

  3. generalize lemma argument

    @eric-wieser
    eric-wieser committed Dec 15, 2021
    Configuration menu
    Copy the full SHA
    2d01e46 View commit details
    Browse the repository at this point in the history

  4. finish

    @eric-wieser
    eric-wieser committed Dec 15, 2021
    Configuration menu
    Copy the full SHA
    ccc8ae5 View commit details
    Browse the repository at this point in the history

  5. Fix linter failure.

    @jsm28
    jsm28 committed Dec 15, 2021
    Configuration menu
    Copy the full SHA
    c04fb5e View commit details
    Browse the repository at this point in the history

Commits on Dec 18, 2021

  1. Merge remote-tracking branch 'origin/master' into jsm28/orientation_c… 

    …omp_linear_equiv
    @jsm28
    jsm28 committed Dec 18, 2021
    Configuration menu
    Copy the full SHA
    999c853 View commit details
    Browse the repository at this point in the history

  2. Refactor in terms of orientation.map.

    @jsm28
    jsm28 committed Dec 18, 2021
    Configuration menu
    Copy the full SHA
    71302b9 View commit details
    Browse the repository at this point in the history

Commits on Dec 23, 2021

  1. Update src/linear_algebra/orientation.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @jsm28 @jcommelin
    jsm28 and jcommelin committed Dec 23, 2021
    Configuration menu
    Copy the full SHA
    9063051 View commit details
    Browse the repository at this point in the history