Def ContinuousLinearMap.prodL

Modification history

2026-03-31 20:10

Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean

chore: split `Topology.Algebra.Module.StrongTopology` (#37440)

Modified ContinuousLinearMap.prodL View on Github →

2025-10-26 18:30

Mathlib/Topology/Algebra/Module/StrongTopology.lean

feat(Topology/Algebra/Module): `prod` and `coprod` as `ContinuousLinearEquiv`s (#28906)

Added ContinuousLinearMap.prodL View on Github →