Commit 2022-06-17 23:41 bd6b98b2

View on Github →

feat(linear_algebra/alternating): add more compositional API (#14802) These will be helpful in relating alternating_maps to the exterior_algebra. This adds:

alternating_map.curry_left
alternating_map.const_linear_equiv_of_is_empty
alternating_map.dom_dom_congr

Estimated changes

Modified src/linear_algebra/alternating.lean

modified theorem alternating_map.coe_dom_dom_congr

added def alternating_map.const_linear_equiv_of_is_empty

added def alternating_map.const_of_is_empty

added def alternating_map.curry_left

added def alternating_map.curry_left_linear_map

added theorem alternating_map.curry_left_same

added def alternating_map.dom_dom_congr

added theorem alternating_map.dom_dom_congr_add

added theorem alternating_map.dom_dom_congr_eq_iff

added theorem alternating_map.dom_dom_congr_eq_zero_iff

added def alternating_map.dom_dom_congr_equiv

added theorem alternating_map.dom_dom_congr_perm

added theorem alternating_map.dom_dom_congr_refl

added theorem alternating_map.dom_dom_congr_trans

added theorem alternating_map.dom_dom_congr_zero

added theorem alternating_map.map_vec_cons_add

added theorem alternating_map.map_vec_cons_smul

modified def alternating_map.of_subsingleton