Commit 2026-01-02 15:12 5102018e

View on Github →

chore(Topology/Algebra/Module/LinearMap): deprecate duplicate lemmas (#33341) Now that range and ker take in a LinearMap instead of a LinearMapClass, these lemmas are the same thing as the linear map versions.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

deleted theorem ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range

Modified Mathlib/LinearAlgebra/Projection.lean

added theorem LinearMap.IsIdempotentElem.ker_eq_range_one_sub

added theorem LinearMap.IsIdempotentElem.range_eq_ker_one_sub

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

deleted theorem ContinuousLinearMap.IsIdempotentElem.ker_eq_range

deleted theorem ContinuousLinearMap.IsIdempotentElem.range_eq_ker