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: Reduce scope of LinearOrderedCommGroupWithZero #11716

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - chore: Reduce scope of LinearOrderedCommGroupWithZero #11716

wants to merge 17 commits into from

Commits on Mar 27, 2024

  1. chore: Reduce scope of LinearOrderedCommGroupWithZero 

    Reconstitute the file `Algebra.Order.Monoid.WithZero` from three files:
* `Algebra.Order.Monoid.WithZero.Defs`
* `Algebra.Order.Monoid.WithZero.Basic`
* `Algebra.Order.WithZero`

Avoid importing it in many files. Most uses were just to get `le_zero_iff` to work on `Nat`.
    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    cb5027a View commit details
    Browse the repository at this point in the history

  2. style

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    721542c View commit details
    Browse the repository at this point in the history

  3. fix

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    872f152 View commit details
    Browse the repository at this point in the history

  4. fix

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    001ba78 View commit details
    Browse the repository at this point in the history

  5. fix Data.Fin.Basic

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    c24888f View commit details
    Browse the repository at this point in the history

  6. fix

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    5bb1dde View commit details
    Browse the repository at this point in the history

  7. fix

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    f1a688b View commit details
    Browse the repository at this point in the history

  8. fix

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    d779ef6 View commit details
    Browse the repository at this point in the history

  9. don't specify universe

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    0a8b1f3 View commit details
    Browse the repository at this point in the history

  10. fix Analysis.MeanInequalities

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    2552f29 View commit details
    Browse the repository at this point in the history

  11. fix

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    899ef41 View commit details
    Browse the repository at this point in the history

  12. fix

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    cde786a View commit details
    Browse the repository at this point in the history

  13. fix

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    24964a6 View commit details
    Browse the repository at this point in the history

  14. fix

    @YaelDillies
    YaelDillies committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    442b2dc View commit details
    Browse the repository at this point in the history

Commits on Mar 28, 2024

  1. Merge remote-tracking branch 'origin/master' into kill_order_with_zero

    @YaelDillies
    YaelDillies committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    2dcf9b2 View commit details
    Browse the repository at this point in the history

  2. fix Data.Finset.Basic

    @YaelDillies
    YaelDillies committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    807daa6 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into kill_order_with_zero

    @YaelDillies
    YaelDillies committed Mar 28, 2024
    Configuration menu
    Copy the full SHA
    5322545 View commit details
    Browse the repository at this point in the history