Theorem LinearMap.prod_comp

Modification history

2023-08-23 11:25
Mathlib/LinearAlgebra/Prod.lean
chore: remove autoImplicit in LinearAlgebra (#6634) …
Modified LinearMap.prod_compView on Github →
2023-04-10 15:18
Mathlib/LinearAlgebra/Prod.lean
feat: port Algebra.Module.Projective (#3335)
Added LinearMap.prod_compView on Github →