mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(Matrix/ToLin): fix `Fintype`/`Finite`

Open urkud opened this issue 1 year ago • 0 comments
trafficstars

Also drop a no longer needed [DecidableEq _] argument in 1 lemma. It was needed to generate a computable Fintype (Set.range _) instance but a Finite instance doesn't need it.

Open in Gitpod

urkud avatar Mar 28 '24 04:03 urkud