Def Fintype.toOrderBot

Modification history

2024-05-07 01:05

Mathlib/Data/Fintype/Order.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted Fintype.toOrderBot View on Github →

2023-01-23 07:49

Mathlib/Data/Fintype/Order.lean

feat: port Data.Fintype.Order (#1718)

Added Fintype.toOrderBot View on Github →