Commit 2025-12-26 13:27 d9c5e283

View on Github →

chore(Order/Synonym): use to_dual (#33266)

Estimated changes

modified theorem OrderDual.le_toDual
modified theorem OrderDual.lt_toDual
modified theorem OrderDual.ofDual_le_ofDual
modified theorem OrderDual.ofDual_lt_ofDual
modified theorem OrderDual.ofDual_symm_eq
modified theorem OrderDual.ofDual_toDual
deleted theorem OrderDual.toDual_le
modified theorem OrderDual.toDual_le_toDual
deleted theorem OrderDual.toDual_lt
modified theorem OrderDual.toDual_lt_toDual
modified theorem OrderDual.toDual_ofDual
modified theorem OrderDual.toDual_symm_eq