Commit 2025-07-11 13:07 eca245ce

View on Github →

feat(LinearAlgebra/Projection): add lemmas for linear projections (#26792) This pr adds some lemmas for linear projections.

Estimated changes

Modified Mathlib/LinearAlgebra/Projection.lean

added theorem LinearMap.IsIdempotentElem.comp_eq_right_iff

added theorem LinearMap.IsIdempotentElem.ext

added theorem LinearMap.IsIdempotentElem.mem_range_iff

added theorem LinearMap.IsProj.isIdempotentElem

added theorem LinearMap.IsProj.mem_iff_map_id

added theorem LinearMap.IsProj.submodule_eq_bot_iff

added theorem LinearMap.IsProj.submodule_eq_top_iff

added theorem LinearMap.IsProj.submodule_unique

added theorem LinearMap.IsProj.subtype_comp_codRestrict

added theorem LinearMap.isProj_range_iff_isIdempotentElem