Theorem Sum.lex_flip_iff

Modification history

2026-10-01 14:50
Mathlib/Order/Sum/Order.lean
feat(SetTheory/Ordinal): definition of addition and multiplication (#43588) …
Added Sum.lex_flip_iffView on Github →