Def LinearMap.lsum

Modification history

2024-08-13 13:38

Mathlib/LinearAlgebra/Pi.lean

chore: backports from nightly-testing-2024-08-12 (#15756)

Modified LinearMap.lsum View on Github →

2023-02-14 06:34

Mathlib/LinearAlgebra/Pi.lean

feat: port LinearAlgebra.Pi (#2250)

Added LinearMap.lsum View on Github →