Commit 2026-01-20 13:02 edec8f50

View on Github →

chore(Order/Defs/Unbundled): deprecate IsTotal in favor of core's Std.Total (#33797)

Estimated changes

deleted theorem multiplicative_of_isTotal
modified theorem Ordnode.dual_insert
modified theorem Ordnode.insert'.valid
modified theorem Ordnode.insert.valid
modified theorem Ordnode.insertWith.valid
deleted theorem IsTotal.compRel
deleted theorem IsTotal.not_incompRel
added theorem compRel_of_total
added theorem not_incompRel_of_total
modified theorem cmpLE_eq_cmp
modified theorem cmpLE_swap
modified theorem total_of
deleted theorem IsTotal.directed
added theorem Std.Total.directed
modified theorem inf_eq_minDefault
modified theorem sup_eq_maxDefault
deleted theorem IsTotal.swap
added theorem Std.Total.swap
modified theorem ValuationRing.iff_dvd_total