Def LinearMap.prod

Modification history

2023-04-10 15:18

Mathlib/LinearAlgebra/Prod.lean

feat: port Algebra.Module.Projective (#3335)

Modified LinearMap.prod View on Github →

2023-02-21 15:57

Mathlib/LinearAlgebra/Prod.lean

feat: port LinearAlgebra.Prod (#2415)

Added LinearMap.prod View on Github →