Theorem LinearMap.IsProj.mem_iff_map_id

Modification history

2025-07-11 13:07

Mathlib/LinearAlgebra/Projection.lean

feat(LinearAlgebra/Projection): add lemmas for linear projections (#26792) …

Added LinearMap.IsProj.mem_iff_map_id View on Github →