Zulip Chat Archive
Stream: mathlib4
Topic: Fintype Ordering
Violeta Hernández (Oct 26 2024 at 14:31):
We're missing a Fintype instance for docs#Ordering, where would be the place to put it?
Violeta Hernández (Oct 26 2024 at 14:35):
Do I just chuck it into Mathlib.Data.Fintype.Basic?
Daniel Weber (Oct 27 2024 at 03:02):
Mathlib.Data.Ordering.Basic could also work
Last updated: May 02 2025 at 03:31 UTC