Commit 2026-03-06 01:12 5dfa22a3

View on Github →

feat(ContinuousAlternatingMap): generalize some definitions (#34513)

Estimated changes

Modified Mathlib/Analysis/Normed/Module/Alternating/Basic.lean

deleted def ContinuousAlternatingMap.compContinuousLinearMapCLM

deleted theorem ContinuousAlternatingMap.compContinuousLinearMapCLM_apply

added theorem ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM

deleted def ContinuousLinearEquiv.continuousAlternatingMapCongr

deleted def ContinuousLinearEquiv.continuousAlternatingMapCongrLeft

deleted def ContinuousLinearEquiv.continuousAlternatingMapCongrRight

deleted theorem ContinuousLinearEquiv.continuousAlternatingMapCongrRight_symm

deleted def ContinuousLinearMap.compContinuousAlternatingMapCLM

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

added def ContinuousAlternatingMap.compContinuousLinearMapCLM

added def ContinuousLinearEquiv.continuousAlternatingMapCongr

added def ContinuousLinearEquiv.continuousAlternatingMapCongrLeft

added def ContinuousLinearEquiv.continuousAlternatingMapCongrRight

added theorem ContinuousLinearEquiv.continuousAlternatingMapCongrRight_symm

added def ContinuousLinearMap.compContinuousAlternatingMapCLM