Def LinearMap.piMap

Modification history

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