Commit 2025-05-19 11:56 947ab139

View on Github →

feat(LinearAlgebra): add LinearMap.const (#25008)

Estimated changes

Modified Mathlib/LinearAlgebra/Pi.lean

added def LinearMap.const

added theorem LinearMap.const_apply