Commit 2026-02-18 14:41 416c6c80

View on Github →

feat: define LinearMap.piMap and ContinuousLinearMap.piMap (#35430) As requested by @eric-wieser in #34491

Estimated changes

added theorem LinearMap.coe_piMap
added def LinearMap.piMap