Theorem LinearPMap.map_smulₛₗ

Modification history

2026-04-03 14:10
Mathlib/LinearAlgebra/LinearPMap.lean
refactor(LinearAlgebra/LinearPMap): generalize (partially) to semilinear maps (#36721) …
Added LinearPMap.map_smulₛₗView on Github →