Commit 2023-07-10 15:31 63e0da05

View on Github →

feat: forward port leanprover-community/mathlib#19128 (#5791)

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

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

modified def ContinuousLinearEquiv.arrowCongrSL

added theorem ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply

added theorem ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply

deleted def ContinuousLinearEquiv.arrowCongrₛₗ

deleted theorem ContinuousLinearEquiv.arrowCongrₛₗ_continuous

added def ContinuousLinearMap.postcomp

added def ContinuousLinearMap.precomp

Modified Mathlib/Topology/VectorBundle/Hom.lean