Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-06 00:12 c2a0532f

View on Github →

feat(logic/unique,data/fintype/basic): unique and fintype of subtype of one element (#8491) Additionally, a lemma proving that the cardinality of such a subtype is 1.

Estimated changes