Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-14 18:03 1b51fe0f

View on Github →

feat(linear_algebra/alternating): add alternating_map.comp_linear_map (#10314)

Estimated changes

Modified src/linear_algebra/alternating.lean

added theorem alternating_map.add_comp_linear_map

added theorem alternating_map.coe_comp_linear_map

added def alternating_map.comp_linear_map

added theorem alternating_map.comp_linear_map_apply

added theorem alternating_map.comp_linear_map_zero

added theorem alternating_map.zero_comp_linear_map