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(Algebra/TensorAlgebra): support towers of algebras #6073

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(Algebra/TensorAlgebra): support towers of algebras #6073

wants to merge 17 commits into from

Commits on Jul 23, 2023

  1. tidy universe variables

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    64b9342 View commit details
    Browse the repository at this point in the history

  2. feat: add scalar tower instances for RingQuot and BilinForm

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    23a1289 View commit details
    Browse the repository at this point in the history

  3. feat(Algebra/FreeAlgebra): support towers of algebras 

    This provide `Algebra R (FreeAlgebra A X)` when `Algebra R A`.
This also fixes some diamonds that would arise as a result of this new instance.
    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    534225e View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/eric-wieser/ringquot-tower' into… 

    … eric-wieser/tower-FreeAlgebra
    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    02860bf View commit details
    Browse the repository at this point in the history

  5. wip

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    72ecf11 View commit details
    Browse the repository at this point in the history

  6. remove unused argument. The linter did not find it :(

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    5bd526b View commit details
    Browse the repository at this point in the history

  7. fix more diamonds

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    b81c037 View commit details
    Browse the repository at this point in the history

  8. sorried for now

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    8514db7 View commit details
    Browse the repository at this point in the history

  9. fix diamonds

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    e1494c8 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'eric-wieser/tower-FreeAlgebra' into eric-wieser/tower-T… 

    …ensorAlgebra
    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    559f0da View commit details
    Browse the repository at this point in the history

  11. deduplicate

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    58ce2c8 View commit details
    Browse the repository at this point in the history

  12. fixed

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    6a0b002 View commit details
    Browse the repository at this point in the history

  13. fix indents

    @eric-wieser
    eric-wieser committed Jul 23, 2023
    Configuration menu
    Copy the full SHA
    7994589 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2023

  1. Merge commit '95a48b5184be1fff2e29807ff28ef377e2872c5b' into eric-wie… 

    …ser/ringquot-tower
    @eric-wieser
    eric-wieser committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    181200c View commit details
    Browse the repository at this point in the history

  2. Merge branch 'eric-wieser/ringquot-tower' into eric-wieser/tower-Tens… 

    …orAlgebra
    @eric-wieser
    eric-wieser committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    9aae83e View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into eric-wieser/tower-T… 

    …ensorAlgebra
    @eric-wieser
    eric-wieser committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    5dd4831 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Algebra/RingQuot.lean

    @eric-wieser
    eric-wieser authored Jul 24, 2023
    Configuration menu
    Copy the full SHA
    b0e9a79 View commit details
    Browse the repository at this point in the history