Commit 2022-12-07 12:38 d89dd2a9

View on Github →

feat port: Order.Antisymmetrization (#876) Mathlib SHA f1a2caaf51ef593799107fe9a8d5e411599f3996 There were a bunch of changes from toAntisymmetrization (. ≤ .) to @toAntisymmetrization α (· ≤ ·) _ and also the coercion to fun for OrderIso.dualAntisymmetrization α did not trigger without making α explicit, previously there was an underscore in place of α

Estimated changes