Commit 2025-03-13 06:42 0b9bf05f

View on Github →

feat(Finpartition): add constructor using existsUnique (#22807)

Estimated changes

Modified Mathlib/Order/Partition/Finpartition.lean

added def Finpartition.ofExistsUnique

added theorem Finpartition.subset