mathlib
655994e2 - refactor(data/set/n_ary): extract from data/set/basic (#17836)

Commit
3 years ago
refactor(data/set/n_ary): extract from data/set/basic (#17836) This is essentially just a copy paste, with one or two whitespace fixes. This split is consistent with how `finset/n_ary` is its own file, and does a nice job of making `data/set/basic` a bit shorter. The comment fixes referring to this new file are thanks to #17825.
Author
Parents
Loading