Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-13 02:38 ac7a356a

View on Github →

chore(set_theory/*): Fix lint (#13399) Add missing docstrings and inhabited instances or a nolint when an inhabited instance isn't reasonable.

Estimated changes