Theorem LinearMap.coe_piMap

Modification history

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