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

Clean up quotient APIs #16210

Draft
wants to merge 17 commits into
base: master
Choose a base branch
from
Draft

Clean up quotient APIs #16210

wants to merge 17 commits into from
+1,015 −1,114

Commits on Aug 28, 2024

  1. Clean up quotient APIs

    @FR-vdash-bot
    FR-vdash-bot committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    adc2cb5 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into FR_quot

    @FR-vdash-bot
    FR-vdash-bot committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    72e27ec View commit details
    Browse the repository at this point in the history

  3. wip

    @FR-vdash-bot
    FR-vdash-bot committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    7f8c9ea View commit details
    Browse the repository at this point in the history

  4. do not need Setoid.Rel

    @FR-vdash-bot
    FR-vdash-bot committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    0f18387 View commit details
    Browse the repository at this point in the history

  5. wip

    @FR-vdash-bot
    FR-vdash-bot committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    0408fd9 View commit details
    Browse the repository at this point in the history

  6. wip

    @FR-vdash-bot
    FR-vdash-bot committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    481b3af View commit details
    Browse the repository at this point in the history

  7. wip

    @FR-vdash-bot
    FR-vdash-bot committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    27e5ef5 View commit details
    Browse the repository at this point in the history

  8. wip

    @FR-vdash-bot
    FR-vdash-bot committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    052eaa7 View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2024

  1. wip

    @FR-vdash-bot
    FR-vdash-bot committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    f5787a4 View commit details
    Browse the repository at this point in the history

  2. done?

    @FR-vdash-bot
    FR-vdash-bot committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    07d245e View commit details
    Browse the repository at this point in the history

  3. Update CliffordAlgebraNotInjective.lean

    @FR-vdash-bot
    FR-vdash-bot committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    425bbf7 View commit details
    Browse the repository at this point in the history

  4. lint

    @FR-vdash-bot
    FR-vdash-bot committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    c0d07be View commit details
    Browse the repository at this point in the history

  5. fix test

    @FR-vdash-bot
    FR-vdash-bot committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    e65615f View commit details
    Browse the repository at this point in the history

  6. fix

    @FR-vdash-bot
    FR-vdash-bot committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    10b4708 View commit details
    Browse the repository at this point in the history

  7. [] -> {}

    @FR-vdash-bot
    FR-vdash-bot committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    570596a View commit details
    Browse the repository at this point in the history

  8. fix

    @FR-vdash-bot
    FR-vdash-bot committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    4ae7e83 View commit details
    Browse the repository at this point in the history

Commits on Sep 2, 2024

  1. Merge branch 'master' into FR_quot

    @FR-vdash-bot
    FR-vdash-bot committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    aa203fb View commit details
    Browse the repository at this point in the history