Def ContinuousLinearMap.piMap

Modification history

2026-02-18 14:41

Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

feat: define `LinearMap.piMap` and `ContinuousLinearMap.piMap` (#35430) …

Added ContinuousLinearMap.piMap View on Github →