Commit 2025-01-26 15:45 0d39cc61

View on Github →

feat(LinearAlgebra/ExteriorPower): the exterior powers, as functors (#18596) We define the nth exterior power functor, from ModuleCat R to itself.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean

added theorem ModuleCat.AlternatingMap.ext

added def ModuleCat.AlternatingMap.postcomp

added theorem ModuleCat.AlternatingMap.postcomp_apply

added def ModuleCat.AlternatingMap

added theorem ModuleCat.exteriorPower.desc_mk

added theorem ModuleCat.exteriorPower.hom_ext

added theorem ModuleCat.exteriorPower.map_mk

added def ModuleCat.exteriorPower.mk

added def ModuleCat.exteriorPower

Modified Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

added theorem exteriorPower.alternatingMapLinearEquiv_symm_map

added theorem exteriorPower.map_apply_ιMulti

added theorem exteriorPower.map_comp

added theorem exteriorPower.map_comp_ιMulti

added theorem exteriorPower.map_id