Commit 2026-08-10 08:17 f7442295

View on Github →

chore(Data/List/MinMax): use to_dual (#41559) This PR uses to_dual to translate some theorems about maxima and minima on lists.

Estimated changes

deleted theorem List.Perm.minimum_eq
deleted def List.argmin
deleted theorem List.argmin_concat
deleted theorem List.argmin_cons
deleted theorem List.argmin_eq_none
deleted theorem List.argmin_eq_some_iff
deleted theorem List.argmin_mem
deleted theorem List.argmin_nil
deleted theorem List.argmin_singleton
deleted theorem List.foldr_min_of_ne_nil
deleted theorem List.index_of_argmin
deleted theorem List.le_min_of_forall_le
deleted theorem List.le_of_mem_argmin
deleted theorem List.mem_argmin_iff
deleted theorem List.min_le_of_le'
deleted theorem List.min_le_of_le
deleted def List.minimum
deleted theorem List.minimum_anti
deleted theorem List.minimum_append
deleted theorem List.minimum_concat
deleted theorem List.minimum_cons
deleted theorem List.minimum_eq_coe_iff
deleted theorem List.minimum_eq_top
deleted theorem List.minimum_le_coe_iff
deleted theorem List.minimum_le_of_mem'
deleted theorem List.minimum_le_of_mem
deleted theorem List.minimum_mem
deleted theorem List.minimum_nil
deleted theorem List.minimum_singleton
deleted theorem List.not_lt_of_mem_argmin