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] - chore: Matrix.mulVec and Matrix.vecMul get infix notation #10297

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - chore: Matrix.mulVec and Matrix.vecMul get infix notation #10297

wants to merge 15 commits into from

Commits on Feb 6, 2024

  1. chore: Matrix.mulVec and Matrix.vecMul get infix notation

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    88e2adb View commit details
    Browse the repository at this point in the history

  2. this was a bug

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    cc6e7d6 View commit details
    Browse the repository at this point in the history

  3. removed redundant parentheses

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    0f460e7 View commit details
    Browse the repository at this point in the history

  4. removed redundant parentheses

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    94d90fa View commit details
    Browse the repository at this point in the history

  5. bugfix

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    4f644f0 View commit details
    Browse the repository at this point in the history

  6. use new notation in RingTheory/Discriminant

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    3f0b545 View commit details
    Browse the repository at this point in the history

  7. more files refactored

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    e59c8b5 View commit details
    Browse the repository at this point in the history

  8. more

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    8459aa5 View commit details
    Browse the repository at this point in the history

  9. comment about precedence

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    adeb3fd View commit details
    Browse the repository at this point in the history

  10. Update Mathlib/LinearAlgebra/Matrix/LDL.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @madvorak @eric-wieser
    madvorak and eric-wieser authored Feb 6, 2024
    Configuration menu
    Copy the full SHA
    ee7d228 View commit details
    Browse the repository at this point in the history

  11. Update Mathlib/Data/Matrix/Notation.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @madvorak @eric-wieser
    madvorak and eric-wieser authored Feb 6, 2024
    Configuration menu
    Copy the full SHA
    86f3861 View commit details
    Browse the repository at this point in the history

  12. parentheses around of removed

    Martin Dvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    777ef27 View commit details
    Browse the repository at this point in the history

  13. should have been in the previous commit

    Martin Dvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    e05d6a3 View commit details
    Browse the repository at this point in the history

  14. mentioned new notation in module docstring

    Martin Dvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    ff21485 View commit details
    Browse the repository at this point in the history

  15. docstring for mulVec and vecMul

    @madvorak
    madvorak committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    830fcd8 View commit details
    Browse the repository at this point in the history