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(Data/Matrix): Eliminate ⬝ notation in favor of HMul #6487

Closed
wants to merge 35 commits into from
Closed

[Merged by Bors] - refactor(Data/Matrix): Eliminate ⬝ notation in favor of HMul #6487

wants to merge 35 commits into from

Commits on Aug 10, 2023

  1. refactor(Data/Matrix): Eliminate ⬝ notation in favor of HMul

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    73af7a2 View commit details
    Browse the repository at this point in the history

  2. purge mul_eq_mul

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    1f2b6f0 View commit details
    Browse the repository at this point in the history

  3. fixes

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    3b7ac23 View commit details
    Browse the repository at this point in the history

  4. fixes

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    7578ea5 View commit details
    Browse the repository at this point in the history

  5. fix

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    a27cbe2 View commit details
    Browse the repository at this point in the history

  6. fixes

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    566089c View commit details
    Browse the repository at this point in the history

  7. fix

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    00ea9c8 View commit details
    Browse the repository at this point in the history

  8. fix

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    12b3826 View commit details
    Browse the repository at this point in the history

  9. fix

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    13b3011 View commit details
    Browse the repository at this point in the history

  10. more fixes

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    0c1e724 View commit details
    Browse the repository at this point in the history

  11. almost there

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    0a39a2a View commit details
    Browse the repository at this point in the history

  12. remove one more Matrix.mul_eq_mul

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    56979dd View commit details
    Browse the repository at this point in the history

  13. default_instance

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    c8bb4c7 View commit details
    Browse the repository at this point in the history

  14. cleanup

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    5dbe451 View commit details
    Browse the repository at this point in the history

  15. fix

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    ff001b0 View commit details
    Browse the repository at this point in the history

  16. workaround for default_instance

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    0620157 View commit details
    Browse the repository at this point in the history

  17. working

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    8b9d741 View commit details
    Browse the repository at this point in the history

  18. lintfix

    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    7c9c4b8 View commit details
    Browse the repository at this point in the history

  19. Merge remote-tracking branch 'origin/master' into eric-wieser/down-wi… 

    …th-⬝
    @eric-wieser
    eric-wieser committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    b5a2b4a View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2023

  1. Update Mathlib/Analysis/NormedSpace/Spectrum.lean 

    Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
    @eric-wieser @joneugster
    eric-wieser and joneugster committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    5395f1d View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Analysis/Normed/Group/Basic.lean 

    Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
    @eric-wieser @joneugster
    eric-wieser and joneugster committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    9dc41ea View commit details
    Browse the repository at this point in the history

  3. Apply suggestions from code review 

    Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
    @eric-wieser @joneugster
    eric-wieser and joneugster committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    42f06b8 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into eric-wieser/down-wi… 

    …th-⬝
    @eric-wieser
    eric-wieser committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    e05d499 View commit details
    Browse the repository at this point in the history

  5. clean up Data/Matrix/Invertible.lean

    @eric-wieser
    eric-wieser committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    dfcbd6f View commit details
    Browse the repository at this point in the history

  6. revert accidental changes to Topology/Homotopy/Product

    @eric-wieser
    eric-wieser committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    51168fb View commit details
    Browse the repository at this point in the history

  7. docstring fixes

    @eric-wieser
    eric-wieser committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    a488326 View commit details
    Browse the repository at this point in the history

  8. revert unrelated docstring changes

    @eric-wieser
    eric-wieser committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    2fd80ba View commit details
    Browse the repository at this point in the history

  9. fix cdot character in unrelated docstring

    @eric-wieser
    eric-wieser committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    81800a2 View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2023

  1. Merge branch 'master' into eric-wieser/down-with-⬝

    @eric-wieser
    eric-wieser committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    44596c5 View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2023

  1. fix

    @eric-wieser
    eric-wieser committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    dc7c10d View commit details
    Browse the repository at this point in the history

  2. update issue comments

    @eric-wieser
    eric-wieser committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    574934b View commit details
    Browse the repository at this point in the history

  3. partial fixes

    @eric-wieser
    eric-wieser committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    7919382 View commit details
    Browse the repository at this point in the history

  4. fixed

    @eric-wieser
    eric-wieser committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    9f5b98a View commit details
    Browse the repository at this point in the history

  5. stray whitespace

    @eric-wieser
    eric-wieser committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    8e36ad1 View commit details
    Browse the repository at this point in the history

  6. one more fix

    @eric-wieser
    eric-wieser committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    669ae64 View commit details
    Browse the repository at this point in the history