Commit 2025-04-23 13:25 4b319309

View on Github →

chore(Topology/Algebra/Module/Alternating): rename some equivs (#24159)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

deleted def ContinuousLinearEquiv.compContinuousMultilinearMapL

deleted theorem ContinuousLinearEquiv.compContinuousMultilinearMapL_apply

deleted theorem ContinuousLinearEquiv.compContinuousMultilinearMapL_symm

added def ContinuousLinearEquiv.continuousMultilinearMapCongrLeft

added theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply

added theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm

added def ContinuousLinearEquiv.continuousMultilinearMapCongrRight

added theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply

added theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm

deleted def ContinuousMultilinearMap.compContinuousLinearMapEquivL

deleted theorem ContinuousMultilinearMap.compContinuousLinearMapEquivL_apply

deleted theorem ContinuousMultilinearMap.compContinuousLinearMapEquivL_symm

Modified Mathlib/Topology/Algebra/Module/Alternating/Basic.lean

deleted def ContinuousLinearEquiv.compContinuousAlternatingMap

deleted def ContinuousLinearEquiv.continuousAlternatingMapComp

deleted def ContinuousLinearEquiv.continuousAlternatingMapCongr

added def ContinuousLinearEquiv.continuousAlternatingMapCongrEquiv

added def ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv

added def ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv