Commit 2025-06-24 15:28 1dd7c685

View on Github →

chore: add ContinuousLinearEquiv.prodAssoc (#26082) This PR continues the work from #25522. Original PR: https://github.com/leanprover-community/mathlib4/pull/25522

Estimated changes

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

added theorem ContinuousLinearEquiv.coe_prodAssoc

added def ContinuousLinearEquiv.prodAssoc

added theorem ContinuousLinearEquiv.prodAssoc_apply

added theorem ContinuousLinearEquiv.prodAssoc_symm_apply

added theorem ContinuousLinearEquiv.prodAssoc_toLinearEquiv