Mathlib Changelog
v4
Changelog
About
Github
Def
Finpartition.ofExistsUnique
Modification history
2025-03-13 06:42
Mathlib/Order/Partition/Finpartition.lean
feat(Finpartition): add constructor using existsUnique (#22807)
Added
Finpartition.ofExistsUnique
View on Github →