Def Fintype.ofIsEmpty

Modification history

2025-02-17 17:27

Mathlib/Data/Fintype/Basic.lean

chore(Data/Fintype): split `Data/Fintype/Basic.lean` (#21831) …

Modified Fintype.ofIsEmpty View on Github →

2023-12-18 10:05

Mathlib/Data/Fintype/Basic.lean

feat: demote the instance Fintype.ofIsEmpty to a def (#8816) …

Added Fintype.ofIsEmpty View on Github →