mathlib
6c046c75 - chore(data/setoid): split into `basic` and `partition` (#2853)

Commit

5 years ago

chore(data/setoid): split into `basic` and `partition` (#2853) The `basic` part has slightly fewer dependencies and `partition` part is never used in `mathlib`.

Author

urkud

Parents

543ae52c

mathlib 6c046c75 - chore(data/setoid): split into `basic` and `partition` (#2853)

mathlib
6c046c75 - chore(data/setoid): split into `basic` and `partition` (#2853)