Theorem LinearMap.const_apply

Modification history

2026-10-27 00:37
Mathlib/Algebra/Module/Pi.lean
chore(Algebra): move `LinearMap.proj` and `LinearMap.pi` (#45302) …
Modified LinearMap.const_applyView on Github →
2025-05-19 11:56
Mathlib/LinearAlgebra/Pi.lean
feat(LinearAlgebra): add `LinearMap.const` (#25008)
Added LinearMap.const_applyView on Github →