Theorem LinearPMap.coe_toFun_eq_coe

Modification history

2026-08-16 23:56
Mathlib/LinearAlgebra/LinearPMap.lean
feat(LinearAlgebra): kernel of a `LinearPMap` (#42423) …
Added LinearPMap.coe_toFun_eq_coeView on Github →