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 α