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: port LinearAlgebra.Prod #2415

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: port LinearAlgebra.Prod #2415

wants to merge 12 commits into from

Commits on Feb 21, 2023

  1. feat: port LinearAlgebra.Prod

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    f9d62c7 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    dea5875 View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    978e206 View commit details
    Browse the repository at this point in the history

  4. most is fixed

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    f13eaa1 View commit details
    Browse the repository at this point in the history

  5. auto: naming

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    6ed00c4 View commit details
    Browse the repository at this point in the history

  6. more fixes

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    5492440 View commit details
    Browse the repository at this point in the history

  7. auto: lint fixes

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    7762aba View commit details
    Browse the repository at this point in the history

  8. more fixes

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    969e0ee View commit details
    Browse the repository at this point in the history

  9. even more fixes

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    817a63d View commit details
    Browse the repository at this point in the history

  10. remove include keyword that was gobbled up by notation

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    6111fd1 View commit details
    Browse the repository at this point in the history

  11. long line

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    48458b5 View commit details
    Browse the repository at this point in the history

  12. fix coe

    @jcommelin
    jcommelin committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    2f6473e View commit details
    Browse the repository at this point in the history