Commit 2025-03-01 20:11 b50b1290

View on Github →

chore(Order/Fin): move coe_max/coe_min (#22448) Also deprecate coe_sup/coe_inf, since they're syntatically the same as coe_max/coe_min now.

Estimated changes

Modified Mathlib/Order/Fin/Basic.lean

added theorem Fin.coe_max

added theorem Fin.coe_min

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

deleted theorem Fin.coe_inf

deleted theorem Fin.coe_max

deleted theorem Fin.coe_min

deleted theorem Fin.coe_sup