basic): add `card_unique` and a warning note to `card_of_subsingleton` (#7008)

Commit

4 years ago

chore(data/fintype/basic): add `card_unique` and a warning note to `card_of_subsingleton` (#7008)

Author

eric-wieser

Parents