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_piMap'View on Github →