Commit 2025-05-27 14:51 26e169e2
View on Github →feat: congruence in the domain and codomain of MultilinearMap (#25142) I found myself wanting these in #25141 We already have some of these results with inconsistent names elsewhere; for now this just adds crosslinks, we can unify the names later. The names are a little inconsistent here; for the domain we have:
LinearEquiv.multilinearMapCongrLeft
(new in this PR)AlternatingMap.domLCongr
ContinuousLinearEquiv.continuousMultilinearMapCongrRight
ContinuousLinearEquiv.continuousAlternatingMapCongrLeft
ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv
(not a linear equiv) and for the range:
LinearEquiv.multilinearMapCongrRight
(new in this PR)LinearEquiv.alternatingMapCongrRight
(new in this PR)ContinuousLinearEquiv.continuousMultilinearMapCongrRight
ContinuousLinearEquiv.continuousAlternatingMapCongrRight