Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 10:30 104fb22c

View on Github →

chore(logic/basic): generalize eq_iff_true_of_subsingleton to Sort (#7061)

Estimated changes

modified theorem eq_iff_true_of_subsingleton