Commit 2020-12-11 10:57 6288eeda
View on Github →feat(linear_algebra/alternating): Add alternatization of multilinear_map (#5187) This adds:
def multilinear_map.alternatize
lemma alternating_map.to_multilinear_map_alternize
feat(linear_algebra/alternating): Add alternatization of multilinear_map (#5187) This adds:
def multilinear_map.alternatize
lemma alternating_map.to_multilinear_map_alternize