Commit 2025-10-26 18:30 e771c6fa

View on Github →

feat(Topology/Algebra/Module): prod and coprod as ContinuousLinearEquivs (#28906)

Estimated changes

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

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

added def ContinuousLinearMap.coprodEquivL

added def ContinuousLinearMap.prodL