Commit 2025-09-05 13:47 3c512956

View on Github →

chore(LinearAlgebra/Projection): deprecating subtype ∘ linearProjOfIsCompl in favor of IsCompl.projection (#27644) This deprecates all instances of U.subtype ∘ U.linearProjOfIsCompl V hUV and (U.linearProjOfIsCompl V hUV x : E) in favor of hUV.projection and hUV.projection x respectively in LinearAlgebra/Projection and other files.

Estimated changes

Modified Mathlib/Algebra/Lie/LieTheorem.lean

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

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Modified Mathlib/LinearAlgebra/Projection.lean

added theorem Submodule.IsCompl.projection_add_projection_eq_self

added theorem Submodule.IsCompl.projection_eq_self_sub_projection

added theorem Submodule.coe_linearProjOfIsCompl_apply

deleted theorem Submodule.linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self

deleted theorem Submodule.linearProjOfIsCompl_eq_self_iff

deleted theorem Submodule.linearProjOfIsCompl_eq_self_sub_linearProjOfIsCompl

deleted theorem Submodule.linearProjOfIsCompl_idempotent

added theorem Submodule.linearProjOfIsCompl_isCompl_projection