Theorem LinearMap.toPMap_domain

Modification history

2026-04-03 14:10
Mathlib/LinearAlgebra/LinearPMap.lean
refactor(LinearAlgebra/LinearPMap): generalize (partially) to semilinear maps (#36721) …
Modified LinearMap.toPMap_domainView on Github →
2023-06-27 12:11
Mathlib/LinearAlgebra/LinearPMap.lean
forward port 18820 (#5521)
Added LinearMap.toPMap_domainView on Github →