Theorem Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty

Modification history

2024-05-28 17:51
Mathlib/Data/Setoid/Partition.lean
Feat (GroupTheory/GroupAction/Blocks) : blocks for a mul action (#12049) …
Added Set.PairwiseDisjoint.isPartition_of_exists_of_ne_emptyView on Github →