Def LinearMap.prodMapRingHom

Modification history

2024-05-17 19:31
Mathlib/LinearAlgebra/Prod.lean
style: remove all isolated `where` (#12991)
Modified LinearMap.prodMapRingHomView on Github →
2023-02-21 15:57
Mathlib/LinearAlgebra/Prod.lean
feat: port LinearAlgebra.Prod (#2415)
Added LinearMap.prodMapRingHomView on Github →