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 α