Theorem ContinuousLinearMap.coe_piMap

Modification history

2026-02-18 14:41
Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
feat: define `LinearMap.piMap` and `ContinuousLinearMap.piMap` (#35430) …
Added ContinuousLinearMap.coe_piMapView on Github →