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.

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

[Merged by Bors] - feat: Create a partition from an element of Sym #14749

Closed
wants to merge 6 commits into from

Commits on Jul 15, 2024

  1. Non-algebra from #12572

    SashaIr committed Jul 15, 2024
    Configuration menu
    Copy the full SHA
    c4710ff View commit details
    Browse the repository at this point in the history
  2. Remove useless lemma

    SashaIr authored Jul 15, 2024
    Configuration menu
    Copy the full SHA
    bf323ba View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2024

  1. Update Mathlib/Combinatorics/Enumerative/Partition.lean

    Co-authored-by: Yaël Dillies <[email protected]>
    SashaIr and YaelDillies authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    5f358a3 View commit details
    Browse the repository at this point in the history
  2. Update Mathlib/Data/Sym/Basic.lean

    Co-authored-by: Yaël Dillies <[email protected]>
    SashaIr and YaelDillies authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    6d16375 View commit details
    Browse the repository at this point in the history
  3. Update Mathlib/Combinatorics/Enumerative/Partition.lean

    Co-authored-by: Yaël Dillies <[email protected]>
    SashaIr and YaelDillies authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    8387417 View commit details
    Browse the repository at this point in the history
  4. Update Mathlib/Combinatorics/Enumerative/Partition.lean

    Co-authored-by: Yaël Dillies <[email protected]>
    SashaIr and YaelDillies authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    021afbf View commit details
    Browse the repository at this point in the history