Commit 2023-06-01 23:29 685595f7

View on Github →

chore: make ι an explicit arg of AlternatingMap.constOfIsEmpty (#4510) Forward-port leanprover-community/mathlib#19123

Estimated changes

modified theorem Basis.det_isEmpty