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] - feat(data/set/finite): Align set.to_finset and set.finite.to_finset #17959

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(data/set/finite): Align set.to_finset and set.finite.to_finset #17959

wants to merge 11 commits into from

Commits on Dec 15, 2022

  1. feat(data/set/finite): Align set.to_finset and set.finite.to_finset

    @YaelDillies
    YaelDillies committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    c7342e7 View commit details
    Browse the repository at this point in the history

  2. done

    @YaelDillies
    YaelDillies committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    025f83a View commit details
    Browse the repository at this point in the history

  3. symm_diff lemmas

    @YaelDillies
    YaelDillies committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    5f8a8ab View commit details
    Browse the repository at this point in the history

  4. dedup to_finset_singleton

    @YaelDillies
    YaelDillies committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    bc132ca View commit details
    Browse the repository at this point in the history

  5. fix data.finset.pointwise

    @YaelDillies
    YaelDillies committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    827d802 View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2022

  1. better lemmas

    @YaelDillies
    YaelDillies committed Dec 16, 2022
    Configuration menu
    Copy the full SHA
    583b088 View commit details
    Browse the repository at this point in the history

  2. fix aliases

    @YaelDillies
    YaelDillies committed Dec 16, 2022
    Configuration menu
    Copy the full SHA
    1cf1354 View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2023

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

    @YaelDillies
    YaelDillies committed Jan 5, 2023
    Configuration menu
    Copy the full SHA
    1a09a71 View commit details
    Browse the repository at this point in the history

  2. fix analysis.analytic.inverse

    @YaelDillies
    YaelDillies committed Jan 5, 2023
    Configuration menu
    Copy the full SHA
    2076644 View commit details
    Browse the repository at this point in the history

Commits on Jan 6, 2023

  1. finish fixing it

    @YaelDillies
    YaelDillies committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    7ba3788 View commit details
    Browse the repository at this point in the history

  2. reorder

    @YaelDillies
    YaelDillies committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    d05d1ce View commit details
    Browse the repository at this point in the history