bool_indicator): split to a new file (#17841)

Commit

3 years ago

chore(data/set/bool_indicator): split to a new file (#17841) `data/set/basic` is long, and this definition is almost never used. Let's put it in its own file.

Author

eric-wieser

Parents

7ab3af8f

mathlib a43fe8bc - chore(data/set/bool_indicator): split to a new file (#17841)

mathlib
a43fe8bc - chore(data/set/bool_indicator): split to a new file (#17841)