Commit 2025-11-19 22:18 5db9169e

View on Github →

chore(Order/Defs/LinearOrder): use @[to_dual] (#31709) This PR tags the content of Mathlib.Order.Defs.LinearOrder with @[to_dual]. For this to work, we also tag some lemmas used by grind with the @[to_dual] tag.

Estimated changes

deleted theorem max_def'
deleted theorem min_def'
deleted theorem eq_max
deleted theorem le_max_left
deleted theorem le_max_right
deleted theorem max_assoc
deleted theorem max_comm
added theorem max_def'
deleted theorem max_eq_left
deleted theorem max_eq_left_of_lt
deleted theorem max_eq_right
deleted theorem max_eq_right_of_lt
deleted theorem max_le
deleted theorem max_left_comm
deleted theorem max_lt
deleted theorem max_self
added theorem min_def'
modified theorem min_eq_left_of_lt
modified theorem min_eq_right_of_lt
modified theorem min_self