Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-07 15:18 a43fe8bc

View on Github →

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.

Estimated changes