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] - refactor(ring_theory/graded_algebra): use add_submonoid_class to generalize to graded rings #14583

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - refactor(ring_theory/graded_algebra): use add_submonoid_class to generalize to graded rings #14583

wants to merge 25 commits into from

Commits on Jun 6, 2022

  1. refactor(ring_theory/graded_algebra): use add_submonoid_class to ge… 

    …neralize to graded rings

Now tha twe have `add_submonoid_class`, we don't need to consider only families of submodules.
For convenience, this keeps around `graded_algebra` as an alias for `graded_ring` over a family of submodules, as this can help with elaboration here and there.
    @eric-wieser
    eric-wieser committed Jun 6, 2022
    Configuration menu
    Copy the full SHA
    5e1b2e3 View commit details
    Browse the repository at this point in the history

  2. lintfix

    @eric-wieser
    eric-wieser committed Jun 6, 2022
    Configuration menu
    Copy the full SHA
    bbbfbf2 View commit details
    Browse the repository at this point in the history

  3. fix

    @eric-wieser
    eric-wieser committed Jun 6, 2022
    Configuration menu
    Copy the full SHA
    d597e57 View commit details
    Browse the repository at this point in the history

  4. fix

    @eric-wieser
    eric-wieser committed Jun 6, 2022
    Configuration menu
    Copy the full SHA
    99a8b7e View commit details
    Browse the repository at this point in the history

  5. fix

    @eric-wieser
    eric-wieser committed Jun 6, 2022
    Configuration menu
    Copy the full SHA
    25b5ee3 View commit details
    Browse the repository at this point in the history

Commits on Jun 8, 2022

  1. feat(algebra/direct_sum/decomposition): add decompositions into a dir… 

    …ect sum

This is a constructive version of `direct_sum.is_internal`, and generalizes the existing `graded_algebra`.
    @eric-wieser
    eric-wieser committed Jun 8, 2022
    Configuration menu
    Copy the full SHA
    b6f2bc9 View commit details
    Browse the repository at this point in the history

  2. fix

    @eric-wieser
    eric-wieser committed Jun 8, 2022
    Configuration menu
    Copy the full SHA
    ba0c574 View commit details
    Browse the repository at this point in the history

  3. lintfix

    @eric-wieser
    eric-wieser committed Jun 8, 2022
    Configuration menu
    Copy the full SHA
    0af1d71 View commit details
    Browse the repository at this point in the history

  4. fix test

    @eric-wieser
    eric-wieser committed Jun 8, 2022
    Configuration menu
    Copy the full SHA
    15a6372 View commit details
    Browse the repository at this point in the history

Commits on Jun 9, 2022

  1. remove graded_algebra.support

    @eric-wieser
    eric-wieser committed Jun 9, 2022
    Configuration menu
    Copy the full SHA
    1b9bc96 View commit details
    Browse the repository at this point in the history

  2. Fix lemma names

    @eric-wieser
    eric-wieser committed Jun 9, 2022
    Configuration menu
    Copy the full SHA
    ebe4954 View commit details
    Browse the repository at this point in the history

  3. Fix

    @eric-wieser
    eric-wieser committed Jun 9, 2022
    Configuration menu
    Copy the full SHA
    4f5d570 View commit details
    Browse the repository at this point in the history

  4. Fix build errors

    @eric-wieser
    eric-wieser committed Jun 9, 2022
    Configuration menu
    Copy the full SHA
    82f500a View commit details
    Browse the repository at this point in the history

Commits on Jun 10, 2022

  1. fix

    @jjaassoonn
    jjaassoonn committed Jun 10, 2022
    Configuration menu
    Copy the full SHA
    4736ecb View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2022

  1. Merge remote-tracking branch 'origin/eric-wieser/direct_sum.decomposi… 

    …tion' into eric-wieser/graded_ring
    @eric-wieser
    eric-wieser committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    8837578 View commit details
    Browse the repository at this point in the history

  2. golf

    @eric-wieser
    eric-wieser committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    450579d View commit details
    Browse the repository at this point in the history

  3. fix

    @jjaassoonn
    jjaassoonn committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    5dac9dc View commit details
    Browse the repository at this point in the history

  4. shorten line

    @jjaassoonn
    jjaassoonn committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    9b2658c View commit details
    Browse the repository at this point in the history

Commits on Jun 15, 2022

  1. expand docstring

    @eric-wieser
    eric-wieser committed Jun 15, 2022
    Configuration menu
    Copy the full SHA
    7016b08 View commit details
    Browse the repository at this point in the history

Commits on Jun 16, 2022

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/direct_… 

    …sum.decomposition
    @eric-wieser
    eric-wieser committed Jun 16, 2022
    Configuration menu
    Copy the full SHA
    43486b8 View commit details
    Browse the repository at this point in the history

  2. fix timeout and golf

    @eric-wieser
    eric-wieser committed Jun 16, 2022
    Configuration menu
    Copy the full SHA
    fe0c699 View commit details
    Browse the repository at this point in the history

Commits on Jun 17, 2022

  1. Merge remote-tracking branch 'origin/master' into HEAD

    @eric-wieser
    eric-wieser committed Jun 17, 2022
    Configuration menu
    Copy the full SHA
    1610418 View commit details
    Browse the repository at this point in the history

  2. Merge commit 'HEAD@{1}' into eric-wieser/graded_ring

    @eric-wieser
    eric-wieser committed Jun 17, 2022
    Configuration menu
    Copy the full SHA
    f4ae5e1 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2022

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/graded_… 

    …ring
    @eric-wieser
    eric-wieser committed Jun 29, 2022
    Configuration menu
    Copy the full SHA
    ab42c0b View commit details
    Browse the repository at this point in the history

  2. rebuild please

    @eric-wieser
    eric-wieser committed Jun 29, 2022
    Configuration menu
    Copy the full SHA
    fbf44e9 View commit details
    Browse the repository at this point in the history