Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alternating_map.coe_comp_linear_map

Modification history

2021-11-14 18:03
src/linear_algebra/alternating.lean
feat(linear_algebra/alternating): add alternating_map.comp_linear_map (#10314)
Added alternating_map.coe_comp_linear_mapView on Github →