Theorem nonempty_fintype

Modification history

2024-12-19 19:41

Mathlib/Data/Fintype/Basic.lean

chore(Fintype): move `nonempty_fintype` (#20053) …

Modified nonempty_fintype View on Github →

2023-08-10 19:52

Mathlib/Data/Fintype/Card.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified nonempty_fintype View on Github →

2023-01-19 11:44

Mathlib/Data/Fintype/Card.lean

feat: port Data.Fintype.Card (#1668)

Added nonempty_fintype View on Github →