Theorem exteriorPower.alternatingMapLinearEquiv_symm_map

Modification history

2025-01-26 15:45
Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
feat(LinearAlgebra/ExteriorPower): the exterior powers, as functors (#18596) …
Added exteriorPower.alternatingMapLinearEquiv_symm_mapView on Github →