Theorem LinearEquiv.fst_comp_prodComm

Modification history

2023-04-20 11:28
Mathlib/LinearAlgebra/Prod.lean
feat: inverse of LinearPMap (#3527)
Added LinearEquiv.fst_comp_prodCommView on Github →