Theorem Finpartition.subset

Modification history

2025-03-13 06:42

Mathlib/Order/Partition/Finpartition.lean

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

Added Finpartition.subset View on Github →