Commit 2025-12-03 01:23 d6f0e1fb

View on Github →

feat(Order/Max): use @[to_dual] (#32059) This PR does the @[to_dual] tagging for Mathlib.Order.Max.

Estimated changes

deleted theorem IsMax.fst
deleted theorem IsMax.mono
deleted theorem IsMax.not_lt
deleted theorem IsMax.prodMk
deleted theorem IsMax.snd
deleted def IsMax
deleted theorem IsTop.fst
deleted theorem IsTop.isMax_iff
deleted theorem IsTop.mono
deleted theorem IsTop.prodMk
deleted theorem IsTop.snd
deleted def IsTop
deleted theorem NoMaxOrder.not_acc
deleted theorem NoTopOrder.to_noMaxOrder
deleted theorem Prod.isMax_iff
deleted theorem Prod.isTop_iff
deleted theorem isMax_iff_forall_not_lt
deleted theorem isMax_ofDual_iff
deleted theorem isMax_toDual_iff
deleted theorem isTop_ofDual_iff
deleted theorem isTop_toDual_iff
deleted theorem noTopOrder_iff_noMaxOrder
deleted theorem not_isMax
deleted theorem not_isMax_iff
deleted theorem not_isMax_of_lt
deleted theorem not_isTop