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(ring_theory/algebra): more on restrict_scalars #2445

Closed
wants to merge 26 commits into from
Closed

[Merged by Bors] - feat(ring_theory/algebra): more on restrict_scalars #2445

wants to merge 26 commits into from

Commits on Apr 18, 2020

  1. [] to {}

    Scott Morrison committed Apr 18, 2020
    Configuration menu
    Copy the full SHA
    a5b3edf View commit details
    Browse the repository at this point in the history

  2. revert unwanted change

    Scott Morrison committed Apr 18, 2020
    Configuration menu
    Copy the full SHA
    cd91bba View commit details
    Browse the repository at this point in the history

  3. revert unwanted change

    Scott Morrison committed Apr 18, 2020
    Configuration menu
    Copy the full SHA
    a8f9ed5 View commit details
    Browse the repository at this point in the history

  4. add comment

    Scott Morrison committed Apr 18, 2020
    Configuration menu
    Copy the full SHA
    dae3ea2 View commit details
    Browse the repository at this point in the history

  5. revert unwanted change

    Scott Morrison committed Apr 18, 2020
    Configuration menu
    Copy the full SHA
    6508d11 View commit details
    Browse the repository at this point in the history

  6. feat(ring_theory/algebra): more on restrict_scalars

    Scott Morrison committed Apr 18, 2020
    Configuration menu
    Copy the full SHA
    b6b3fe7 View commit details
    Browse the repository at this point in the history

  7. Apply suggestions from code review 

    Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @semorrison @sgouezel
    semorrison and sgouezel committed Apr 18, 2020
    Configuration menu
    Copy the full SHA
    503ccae View commit details
    Browse the repository at this point in the history

  8. changes from review

    @semorrison
    semorrison committed Apr 18, 2020
    Configuration menu
    Copy the full SHA
    349f6c4 View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'origin/implicit_args' into restrict_sca… 

    …lars
    @semorrison
    semorrison committed Apr 18, 2020
    Configuration menu
    Copy the full SHA
    0f8ea55 View commit details
    Browse the repository at this point in the history

Commits on Apr 19, 2020

  1. more implicit arguments

    @semorrison
    semorrison committed Apr 19, 2020
    Configuration menu
    Copy the full SHA
    e75858c View commit details
    Browse the repository at this point in the history

  2. Merge branch 'implicit_args' into restrict_scalars

    @semorrison
    semorrison committed Apr 19, 2020
    Configuration menu
    Copy the full SHA
    cc931c5 View commit details
    Browse the repository at this point in the history

  3. type synonym

    @semorrison
    semorrison committed Apr 19, 2020
    Configuration menu
    Copy the full SHA
    59c3480 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into restrict_scalars

    @semorrison
    semorrison committed Apr 19, 2020
    Configuration menu
    Copy the full SHA
    3329c6d View commit details
    Browse the repository at this point in the history

Commits on May 21, 2020

  1. merge

    @semorrison
    semorrison committed May 21, 2020
    Configuration menu
    Copy the full SHA
    8ad0107 View commit details
    Browse the repository at this point in the history

  2. minor

    @semorrison
    semorrison committed May 21, 2020
    Configuration menu
    Copy the full SHA
    8fa7c90 View commit details
    Browse the repository at this point in the history

  3. making S explicit in restrict_scalars

    @semorrison
    semorrison committed May 21, 2020
    Configuration menu
    Copy the full SHA
    08b39f5 View commit details
    Browse the repository at this point in the history

  4. linting

    @semorrison
    semorrison committed May 21, 2020
    Configuration menu
    Copy the full SHA
    52baa18 View commit details
    Browse the repository at this point in the history

Commits on May 22, 2020

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

    @semorrison
    semorrison committed May 22, 2020
    Configuration menu
    Copy the full SHA
    4c35d85 View commit details
    Browse the repository at this point in the history

  2. updates

    @semorrison
    semorrison committed May 22, 2020
    Configuration menu
    Copy the full SHA
    ed1ea6f View commit details
    Browse the repository at this point in the history

  3. fix

    @semorrison
    semorrison committed May 22, 2020
    Configuration menu
    Copy the full SHA
    f697b30 View commit details
    Browse the repository at this point in the history

Commits on May 26, 2020

  1. Update src/ring_theory/algebra.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @semorrison @jcommelin
    semorrison and jcommelin committed May 26, 2020
    Configuration menu
    Copy the full SHA
    e7fb63e View commit details
    Browse the repository at this point in the history

  2. add typeclass arguments to module.restrict_scalars type synonym

    @semorrison
    semorrison committed May 26, 2020
    Configuration menu
    Copy the full SHA
    8f0500f View commit details
    Browse the repository at this point in the history

  3. Merge branch 'restrict_scalars' of github.com:leanprover-community/ma… 

    …thlib into restrict_scalars
    @semorrison
    semorrison committed May 26, 2020
    Configuration menu
    Copy the full SHA
    70d1622 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into restrict_scalars

    @semorrison
    semorrison committed May 26, 2020
    Configuration menu
    Copy the full SHA
    63ab834 View commit details
    Browse the repository at this point in the history

  5. remove typeclass arguments on type synonym again

    @semorrison
    semorrison committed May 26, 2020
    Configuration menu
    Copy the full SHA
    203079f View commit details
    Browse the repository at this point in the history

  6. linting

    @semorrison
    semorrison committed May 26, 2020
    Configuration menu
    Copy the full SHA
    fdd2a1e View commit details
    Browse the repository at this point in the history