Commit 2025-03-28 10:45 56269680

View on Github →

fix(Interval/Finset/Fin): fix a diamond (#23392) Avoid a non-defeq diamond for LocallyFiniteOrderBot (Fin (n + 1)), with another instance coming from LocallyFiniteOrder and OrderBot.

Estimated changes

Modified Mathlib/Order/Interval/Finset/Fin.lean

modified theorem Fin.Iic_eq_finset_subtype

modified theorem Fin.Iio_eq_finset_subtype