Commit 2023-02-22 13:01 bd687854

View on Github →

feat: port LinearAlgebra.Projection (#2431)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Projection.lean

added def LinearMap.IsProj.codRestrict

added theorem LinearMap.IsProj.codRestrict_apply

added theorem LinearMap.IsProj.codRestrict_apply_cod

added theorem LinearMap.IsProj.codRestrict_ker

added theorem LinearMap.IsProj.eq_conj_prodMap

added theorem LinearMap.IsProj.eq_conj_prod_map'

added theorem LinearMap.IsProj.isCompl

added structure LinearMap.IsProj

added theorem LinearMap.coe_equivProdOfSurjectiveOfIsCompl

added def LinearMap.equivProdOfSurjectiveOfIsCompl

added theorem LinearMap.equivProdOfSurjectiveOfIsCompl_apply

added theorem LinearMap.isCompl_of_proj

added theorem LinearMap.isProj_iff_idempotent

added theorem LinearMap.ker_id_sub_eq_of_proj

added theorem LinearMap.linearProjOfIsCompl_of_proj

added def LinearMap.ofIsCompl

added def LinearMap.ofIsComplProd

added def LinearMap.ofIsComplProdEquiv

added theorem LinearMap.ofIsComplProd_apply

added theorem LinearMap.ofIsCompl_add

added theorem LinearMap.ofIsCompl_eq'

added theorem LinearMap.ofIsCompl_eq

added theorem LinearMap.ofIsCompl_left_apply

added theorem LinearMap.ofIsCompl_right_apply

added theorem LinearMap.ofIsCompl_smul

added theorem LinearMap.ofIsCompl_zero

added theorem LinearMap.range_eq_of_proj

added theorem Submodule.coe_isComplEquivProj_apply

added theorem Submodule.coe_isComplEquivProj_symm_apply

added theorem Submodule.coe_prodEquivOfIsCompl'

added theorem Submodule.coe_prodEquivOfIsCompl

added theorem Submodule.existsUnique_add_of_isCompl

added theorem Submodule.existsUnique_add_of_isCompl_prod

added def Submodule.isComplEquivProj

added def Submodule.linearProjOfIsCompl

added theorem Submodule.linearProjOfIsCompl_apply_eq_zero_iff

added theorem Submodule.linearProjOfIsCompl_apply_left

added theorem Submodule.linearProjOfIsCompl_apply_right'

added theorem Submodule.linearProjOfIsCompl_apply_right

added theorem Submodule.linearProjOfIsCompl_comp_subtype

added theorem Submodule.linearProjOfIsCompl_idempotent

added theorem Submodule.linearProjOfIsCompl_ker

added theorem Submodule.linearProjOfIsCompl_range

added theorem Submodule.linear_proj_add_linearProjOfIsCompl_eq_self

added theorem Submodule.mk_quotientEquivOfIsCompl_apply

added theorem Submodule.prodComm_trans_prodEquivOfIsCompl

added def Submodule.prodEquivOfIsCompl

added theorem Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero

added theorem Submodule.prodEquivOfIsCompl_symm_apply_left

added theorem Submodule.prodEquivOfIsCompl_symm_apply_right

added theorem Submodule.prodEquivOfIsCompl_symm_apply_snd_eq_zero

added def Submodule.quotientEquivOfIsCompl

added theorem Submodule.quotientEquivOfIsCompl_apply_mk_coe

added theorem Submodule.quotientEquivOfIsCompl_symm_apply