Commit 2022-06-24 15:26 0e5f278d

View on Github →

feat(linear_algebra/{multilinear, alternating}): add cod_restrict and lemmas (#14927)

Estimated changes

Modified src/linear_algebra/alternating.lean

added def alternating_map.cod_restrict

added theorem linear_map.comp_alternating_map_cod_restrict

added theorem linear_map.subtype_comp_alternating_map_cod_restrict

Modified src/linear_algebra/multilinear/basic.lean

added theorem linear_map.comp_multilinear_map_cod_restrict

added theorem linear_map.subtype_comp_multilinear_map_cod_restrict

added def multilinear_map.cod_restrict