Commit 2024-12-04 19:43 58c96928

feat(LinearAlgebra/ExteriorPower): the universal property of the exterior power (#18590) We obtain the universal property of the nth exterior power of a module M: linear maps from this exterior power identify to n-alternating maps from M. This is also phrased as the data of a presentation of the exterior power by generators and relations.