Commit 2025-08-24 11:37 6f1af37c

View on Github →

feat: add ContinuousLinearEquiv.prodProdProdComm (#28840) In analogy to LinearEquiv.prodProdProdComm. From the path towards smooth immersions, embeddings and embedded submanifolds.

Estimated changes

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

added theorem ContinuousLinearEquiv.coe_prodProdProdComm

added def ContinuousLinearEquiv.prodProdProdComm

added theorem ContinuousLinearEquiv.prodProdProdComm_apply

added theorem ContinuousLinearEquiv.prodProdProdComm_symm

added theorem ContinuousLinearEquiv.prodProdProdComm_toLinearEquiv