Def Partition.Rel

Modification history

2026-04-05 15:16

Mathlib/Order/Partition/Basic.lean

feat(Order/Partition): add `Rel`, relation induced by partition on Set (#36991) …

Added Partition.Rel View on Github →