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(algebra/module/linear_map): Move elementwise structure from linear_algebra/basic #9331

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - refactor(algebra/module/linear_map): Move elementwise structure from linear_algebra/basic #9331

wants to merge 9 commits into from

Commits on Sep 22, 2021

  1. refactor(algebra/module/linear_map): Move elementwise structure from … 

    …linear_algebra/basic

This helps reduce the size of linear_algebra/basic, and by virtue of being a smaller file makes it easier to spot typeclasses which can be relaxed.
In particular, `linear_map.endomorphism_ring` now requires only `semiring R` not `ring R`.
    @eric-wieser
    eric-wieser committed Sep 22, 2021
    Configuration menu
    Copy the full SHA
    5ce1b72 View commit details
    Browse the repository at this point in the history

  2. fix

    @eric-wieser
    eric-wieser committed Sep 22, 2021
    Configuration menu
    Copy the full SHA
    3634565 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2021

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

    …map-arithmetic
    @eric-wieser
    eric-wieser committed Sep 27, 2021
    Configuration menu
    Copy the full SHA
    a05c3f2 View commit details
    Browse the repository at this point in the history

  2. fix merge mistakes

    @eric-wieser
    eric-wieser committed Sep 27, 2021
    Configuration menu
    Copy the full SHA
    0d6d8c7 View commit details
    Browse the repository at this point in the history

  3. golf

    @eric-wieser
    eric-wieser committed Sep 27, 2021
    Configuration menu
    Copy the full SHA
    a49f00f View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2021

  1. Merge remote-tracking branch 'origin/staging' into eric-wieser/linear… 

    …_map-arithmetic

# Conflicts:
#	src/algebra/module/linear_map.lean
#	src/linear_algebra/basic.lean
    @eric-wieser
    eric-wieser committed Sep 29, 2021
    Configuration menu
    Copy the full SHA
    632da29 View commit details
    Browse the repository at this point in the history

  2. tweak

    @eric-wieser
    eric-wieser committed Sep 29, 2021
    Configuration menu
    Copy the full SHA
    1308caf View commit details
    Browse the repository at this point in the history

  3. Fix docstring merge issue

    @eric-wieser
    eric-wieser committed Sep 29, 2021
    Configuration menu
    Copy the full SHA
    09eac4c View commit details
    Browse the repository at this point in the history

  4. long line

    @eric-wieser
    eric-wieser committed Sep 29, 2021
    Configuration menu
    Copy the full SHA
    b58d09e View commit details
    Browse the repository at this point in the history