Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.coe_prod

Modification history

2022-02-09 17:14
src/linear_algebra/prod.lean
chore(data/pi): add pi.prod and use elsewhere (#11877) …
Added linear_map.coe_prodView on Github →