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

Estimated changes