Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-01 13:25 7188eae5

View on Github →

feat(linear_algebra): Add alternating multilinear maps (#5102)

Estimated changes

Created src/linear_algebra/alternating.lean

added theorem alternating_map.add_apply

added theorem alternating_map.coe_inj

added theorem alternating_map.coe_mk

added theorem alternating_map.coe_multilinear_map

added theorem alternating_map.coe_multilinear_map_mk

added theorem alternating_map.congr_arg

added theorem alternating_map.congr_fun

added theorem alternating_map.ext

added theorem alternating_map.ext_iff

added theorem alternating_map.map_add

added theorem alternating_map.map_add_swap

added theorem alternating_map.map_congr_perm

added theorem alternating_map.map_eq_zero_of_eq

added theorem alternating_map.map_perm

added theorem alternating_map.map_smul

added theorem alternating_map.map_sub

added theorem alternating_map.map_swap

added theorem alternating_map.map_swap_add

added theorem alternating_map.map_update_self

added theorem alternating_map.map_update_update

added theorem alternating_map.neg_apply

added theorem alternating_map.smul_apply

added theorem alternating_map.to_fun_eq_coe

added theorem alternating_map.to_multilinear_map_eq_coe

added theorem alternating_map.zero_apply

added structure alternating_map