Def alternating_map.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.comp_linear_mapView on Github →