Mathlib v3 is deprecated. Go to Mathlib v4

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_map View on Github →