mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore: Remove order dependencies to `Data.Fin.Basic`

Open YaelDillies opened this issue 1 year ago • 0 comments

Move all the declarations using the mathlib order hierarchy to a new file Order.Fin. There were a bunch of order embeddings in Data.Fin.Basic, so I kept an embedding version of them around and renamed the order embedding version.

Open in Gitpod

YaelDillies avatar May 18 '24 09:05 YaelDillies