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.
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.