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/Star/*): Allow for star operation on non-associative algebras #6562

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - refactor(Algebra/Star/*): Allow for star operation on non-associative algebras #6562

wants to merge 21 commits into from

Commits on Aug 13, 2023

  1. Remove requirement for star multiplication to be associative

    @mans0954
    mans0954 committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    4d6f4bc View commit details
    Browse the repository at this point in the history

  2. SelfAdjoint

    @mans0954
    mans0954 committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    bf42f7c View commit details
    Browse the repository at this point in the history

  3. Fix Gelfand Duality

    @mans0954
    mans0954 committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    afccfaa View commit details
    Browse the repository at this point in the history

  4. Rename to StarMul

    @mans0954
    mans0954 committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    5a9d78c View commit details
    Browse the repository at this point in the history

  5. Rename StarMul

    @mans0954
    mans0954 committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    04e613a View commit details
    Browse the repository at this point in the history

  6. Fix

    @mans0954
    mans0954 committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    c17be99 View commit details
    Browse the repository at this point in the history

  7. More fixes

    @mans0954
    mans0954 committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    6cc5c7d View commit details
    Browse the repository at this point in the history

  8. Fix

    @mans0954
    mans0954 committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    7b3aec0 View commit details
    Browse the repository at this point in the history

  9. Lint

    @mans0954
    mans0954 committed Aug 13, 2023
    Configuration menu
    Copy the full SHA
    76e436f View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2023

  1. Update Mathlib/Algebra/Star/Basic.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    a8ee66e View commit details
    Browse the repository at this point in the history

  2. Update docstring

    @mans0954
    mans0954 committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    d11789a View commit details
    Browse the repository at this point in the history

  3. Fix

    @mans0954
    mans0954 committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    e6fa411 View commit details
    Browse the repository at this point in the history

  4. More docstring updates

    @mans0954
    mans0954 committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    084ed21 View commit details
    Browse the repository at this point in the history

  5. Update module docstring

    @mans0954
    mans0954 committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    e7c8496 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/Algebra/Star/Basic.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    05a8dc3 View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/Algebra/Star/Basic.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    6c03ef9 View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/Algebra/Star/Basic.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @mans0954 @eric-wieser
    mans0954 and eric-wieser committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    6afc5de View commit details
    Browse the repository at this point in the history

Commits on Aug 21, 2023

  1. Merge commit 'f25139b758e258bad4af67c9e503d4ed82dfd65a' into mans0954… 

    …/non-assoc-star-mul
    @eric-wieser
    eric-wieser committed Aug 21, 2023
    Configuration menu
    Copy the full SHA
    1362a3a View commit details
    Browse the repository at this point in the history

Commits on Aug 31, 2023

  1. Update Mathlib/Algebra/Star/NonUnitalSubalgebra.lean 

    Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
    @mans0954 @j-loreaux
    mans0954 and j-loreaux committed Aug 31, 2023
    Configuration menu
    Copy the full SHA
    70b519e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into mans0954/non-assoc-star-mul

    @mans0954
    mans0954 committed Aug 31, 2023
    Configuration menu
    Copy the full SHA
    5cba03c View commit details
    Browse the repository at this point in the history

  3. Use term magma in docstrings

    @mans0954
    mans0954 committed Aug 31, 2023
    Configuration menu
    Copy the full SHA
    dc20125 View commit details
    Browse the repository at this point in the history