Commit 2026-05-05 16:21 50fb945b

View on Github →

chore(LinearAlgebra/Projection): rename Submodule.linearProjOfIsCompl to Submodule.projectionOnto (#38956) ... also rename Submodule.IsCompl.projection to Submodule.projection and make the submodule variables explicit.

Estimated changes

Modified Mathlib/Algebra/Lie/LieTheorem.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

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

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

deleted theorem Submodule.IsCompl.projection_isSymmetricProjection_iff

deleted theorem Submodule.IsCompl.projection_isSymmetric_iff

added theorem Submodule.isSymmetricProjection_projection_iff

added theorem Submodule.isSymmetric_projection_iff

Modified Mathlib/Analysis/Normed/Module/Complemented.lean

Modified Mathlib/LinearAlgebra/Basis/Exact.lean

deleted theorem Submodule.linearProjOfIsCompl_comp_bijective_of_exact

deleted theorem Submodule.linearProjOfIsCompl_comp_surjective_of_exact

added theorem Submodule.projectionOnto_comp_bijective_of_exact

added theorem Submodule.projectionOnto_comp_surjective_of_exact

Modified Mathlib/LinearAlgebra/Projection.lean

deleted theorem LinearMap.IsIdempotentElem.eq_isCompl_projection

added theorem LinearMap.IsIdempotentElem.eq_projection

deleted theorem LinearMap.isIdempotentElem_iff_eq_isCompl_projection_range_ker

added theorem LinearMap.isIdempotentElem_iff_eq_projection_range_ker

deleted theorem LinearMap.linearProjOfIsCompl_of_proj

added theorem LinearMap.projectionOnto_of_proj

deleted theorem LinearMap.surjective_comp_linearProjOfIsCompl

added theorem LinearMap.surjective_comp_projectionOnto

deleted theorem Submodule.IsCompl.projection_add_projection_eq_id

deleted theorem Submodule.IsCompl.projection_add_projection_eq_self

deleted theorem Submodule.IsCompl.projection_apply

deleted theorem Submodule.IsCompl.projection_apply_eq_zero_iff

deleted theorem Submodule.IsCompl.projection_apply_left

deleted theorem Submodule.IsCompl.projection_apply_mem

deleted theorem Submodule.IsCompl.projection_apply_right

deleted theorem Submodule.IsCompl.projection_eq_id_sub_projection

deleted theorem Submodule.IsCompl.projection_eq_self_iff

deleted theorem Submodule.IsCompl.projection_eq_self_sub_projection

deleted theorem Submodule.IsCompl.projection_isIdempotentElem

deleted theorem Submodule.IsCompl.projection_ker

deleted theorem Submodule.IsCompl.projection_range

deleted theorem Submodule.coe_linearProjOfIsCompl_apply

added theorem Submodule.coe_projectionOnto_apply

added theorem Submodule.isIdempotentElem_projection

added theorem Submodule.ker_projection

added theorem Submodule.ker_projectionOnto

deleted def Submodule.linearProjOfIsCompl

deleted theorem Submodule.linearProjOfIsCompl_apply_eq_zero_iff

deleted theorem Submodule.linearProjOfIsCompl_apply_left

deleted theorem Submodule.linearProjOfIsCompl_apply_right'

deleted theorem Submodule.linearProjOfIsCompl_apply_right

deleted theorem Submodule.linearProjOfIsCompl_comp_subtype

deleted theorem Submodule.linearProjOfIsCompl_isCompl_projection

deleted theorem Submodule.linearProjOfIsCompl_ker

deleted theorem Submodule.linearProjOfIsCompl_range

deleted theorem Submodule.linearProjOfIsCompl_surjective

added def Submodule.projectionOnto

added theorem Submodule.projectionOnto_apply_eq_zero_iff

added theorem Submodule.projectionOnto_apply_left

added theorem Submodule.projectionOnto_apply_right

added theorem Submodule.projectionOnto_comp_subtype

added theorem Submodule.projectionOnto_projection

added theorem Submodule.projectionOnto_surjective

added theorem Submodule.projection_add_projection_eq_id

added theorem Submodule.projection_add_projection_eq_self

added theorem Submodule.projection_apply

added theorem Submodule.projection_apply_eq_zero_iff

added theorem Submodule.projection_apply_left

added theorem Submodule.projection_apply_mem

added theorem Submodule.projection_apply_right

added theorem Submodule.projection_eq_id_sub_projection

added theorem Submodule.projection_eq_self_iff

added theorem Submodule.projection_eq_self_sub_projection

added theorem Submodule.range_projection

added theorem Submodule.range_projectionOnto

Modified Mathlib/RingTheory/SimpleModule/Basic.lean

Modified Mathlib/RingTheory/SimpleModule/Isotypic.lean

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

deleted theorem Submodule.IsCompl.isTopCompl_iff_linearProjOfIsCompl

added theorem Submodule.IsCompl.isTopCompl_iff_projectionOnto

deleted theorem Submodule.IsTopCompl.continuous_linearProjOfIsCompl

added theorem Submodule.IsTopCompl.continuous_projectionOnto

modified theorem Submodule.range_projectionOntoL