Projection

📁 Source: Mathlib/LinearAlgebra/Projection.lean

Statistics

Metric	Count
Definitions `IsProj`, `codRestrict`, `equivProdOfSurjectiveOfIsCompl`, `linearProjOfIsCompl`, `ofIsCompl`, `ofIsComplProd`, `ofIsComplProdEquiv`, `projection`, `isComplEquivProj`, `isIdempotentElemEquiv`, `linearProjOfIsCompl`, `prodEquivOfIsCompl`, `quotientEquivOfIsCompl`	13
Theorems `commute_iff`, `commute_iff_of_isUnit`, `comp_eq_left_iff`, `comp_eq_right_iff`, `conj_eq_of_ker_mem_invtSubmodule`, `conj_eq_of_range_mem_invtSubmodule`, `eq_isCompl_projection`, `ext`, `ext_iff`, `isCompl`, `isProj_range`, `ker_eq_range`, `ker_eq_range_one_sub`, `ker_mem_invtSubmodule`, `ker_mem_invtSubmodule_iff`, `mem_range_iff`, `range_eq_ker`, `range_eq_ker_one_sub`, `range_mem_invtSubmodule`, `range_mem_invtSubmodule_iff`, `bot`, `codRestrict_apply`, `codRestrict_apply_cod`, `codRestrict_ker`, `eq_conj_prodMap`, `eq_conj_prod_map'`, `isCompl`, `isIdempotentElem`, `map_id`, `map_mem`, `mem_iff_map_id`, `mem_invtSubmodule_iff`, `range`, `submodule_eq_bot_iff`, `submodule_eq_top_iff`, `submodule_unique`, `subtype_comp_codRestrict`, `top`, `coe_equivProdOfSurjectiveOfIsCompl`, `equivProdOfSurjectiveOfIsCompl_apply`, `isCompl_of_proj`, `isIdempotentElem_iff_eq_isCompl_projection_range_ker`, `isProj_iff_isIdempotentElem`, `isProj_range_iff_isIdempotentElem`, `ker_id_sub_eq_of_proj`, `ker_linearProjOfIsCompl`, `linearProjOfIsCompl_apply_left`, `linearProjOfIsCompl_apply_right`, `linearProjOfIsCompl_apply_right'`, `linearProjOfIsCompl_of_proj`, `ofIsComplProd_apply`, `ofIsCompl_add`, `ofIsCompl_eq`, `ofIsCompl_eq'`, `ofIsCompl_eq_add`, `ofIsCompl_left_apply`, `ofIsCompl_right_apply`, `ofIsCompl_smul`, `ofIsCompl_subtype_zero_eq`, `ofIsCompl_symm`, `ofIsCompl_zero`, `range_eq_of_proj`, `range_ofIsCompl`, `surjective_comp_linearProjOfIsCompl`, `surjective_comp_subtype_of_isComplemented`, `projection_add_projection_eq_self`, `projection_apply`, `projection_apply_eq_zero_iff`, `projection_apply_left`, `projection_apply_mem`, `projection_eq_self_iff`, `projection_eq_self_sub_projection`, `projection_isIdempotentElem`, `projection_ker`, `projection_range`, `coe_isComplEquivProj_apply`, `coe_isComplEquivProj_symm_apply`, `coe_linearProjOfIsCompl_apply`, `coe_prodEquivOfIsCompl`, `coe_prodEquivOfIsCompl'`, `existsUnique_add_of_isCompl`, `existsUnique_add_of_isCompl_prod`, `isIdempotentElemEquiv_apply_coe`, `isIdempotentElemEquiv_symm_apply_coe`, `linearProjOfIsCompl_apply_eq_zero_iff`, `linearProjOfIsCompl_apply_left`, `linearProjOfIsCompl_apply_right`, `linearProjOfIsCompl_apply_right'`, `linearProjOfIsCompl_comp_subtype`, `linearProjOfIsCompl_isCompl_projection`, `linearProjOfIsCompl_ker`, `linearProjOfIsCompl_range`, `linearProjOfIsCompl_surjective`, `mk_quotientEquivOfIsCompl_apply`, `prodComm_trans_prodEquivOfIsCompl`, `prodEquivOfIsCompl_symm_apply`, `prodEquivOfIsCompl_symm_apply_fst_eq_zero`, `prodEquivOfIsCompl_symm_apply_left`, `prodEquivOfIsCompl_symm_apply_right`, `prodEquivOfIsCompl_symm_apply_snd_eq_zero`, `quotientEquivOfIsCompl_apply_mk_coe`, `quotientEquivOfIsCompl_symm_apply`, `toLinearMap_prodEquivOfIsCompl_symm`	103
Total	116

LinearMap

Definitions

Name	Category	Theorems
`IsProj` 📖	CompData	6 math math: `Representation.isProj_averageMap`, `IsProj.top`, `isProj_range_iff_isIdempotentElem`, `IsIdempotentElem.isProj_range`, `IsProj.bot`, `isProj_iff_isIdempotentElem`
`equivProdOfSurjectiveOfIsCompl` 📖	CompOp	3 math math: `ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_toLinearEquiv`, `coe_equivProdOfSurjectiveOfIsCompl`, `equivProdOfSurjectiveOfIsCompl_apply`
`linearProjOfIsCompl` 📖	CompOp	6 math math: `ker_linearProjOfIsCompl`, `linearProjOfIsCompl_apply_right`, `linearProjOfIsCompl_comp_bijective_of_exact`, `linearProjOfIsCompl_apply_right'`, `linearProjOfIsCompl_apply_left`, `Finsupp.lcomapDomain_eq_linearProjOfIsCompl`
`ofIsCompl` 📖	CompOp	12 math math: `ofIsCompl_symm`, `ofIsCompl_smul`, `ofIsComplProd_apply`, `ofIsCompl_add`, `ofIsCompl_eq'`, `ofIsCompl_eq`, `range_ofIsCompl`, `ofIsCompl_left_apply`, `ofIsCompl_right_apply`, `ofIsCompl_subtype_zero_eq`, `ofIsCompl_zero`, `ofIsCompl_eq_add`
`ofIsComplProd` 📖	CompOp	1 math math: `ofIsComplProd_apply`
`ofIsComplProdEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_equivProdOfSurjectiveOfIsCompl` 📖	mathematical	`range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Top.top` `Submodule` `Submodule.instTop` `IsCompl` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `ker`	`LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Prod.instAddCommMonoid` `Prod.instModule` `equivProdOfSurjectiveOfIsCompl` `prod`	—	`RingHomSurjective.ids` `RingHomInvPair.ids`
`equivProdOfSurjectiveOfIsCompl_apply` 📖	mathematical	`range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Top.top` `Submodule` `Submodule.instTop` `IsCompl` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `ker`	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `equivProdOfSurjectiveOfIsCompl` `LinearMap` `instFunLike`	—	`RingHomSurjective.ids` `RingHomInvPair.ids`
`isCompl_of_proj` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instFunLike`	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `ker` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`disjoint_iff_inf_le` `Submodule.mk_eq_zero` `mem_ker` `SetLike.mem_coe` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `codisjoint_iff_le_sup` `Submodule.mem_sup'` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `sub_self` `add_sub_cancel`
`isIdempotentElem_iff_eq_isCompl_projection_range_ker` 📖	mathematical	—	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `IsCompl` `Submodule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `range` `RingHomSurjective.ids` `ker` `Submodule.IsCompl.projection`	—	`RingHomSurjective.ids` `IsProj.isCompl` `IsIdempotentElem.isProj_range` `IsIdempotentElem.eq_isCompl_projection` `Submodule.IsCompl.projection_isIdempotentElem`
`isProj_iff_isIdempotentElem` 📖	mathematical	—	`Submodule` `IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `IsIdempotentElem` `Module.End.instMul`	—	`ext` `IsProj.map_id` `IsProj.map_mem` `RingHomSurjective.ids` `IsIdempotentElem.isProj_range`
`isProj_range_iff_isIdempotentElem` 📖	mathematical	—	`IsProj` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap` `instFunLike` `IsIdempotentElem` `Module.End.instMul`	—	`RingHomSurjective.ids` `ext` `mem_range_self` `Module.End.mul_apply` `IsIdempotentElem.eq`
`ker_id_sub_eq_of_proj` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instFunLike`	`ker` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap` `instSub` `id` `comp` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHomCompTriple.ids` `Submodule.subtype`	—	`Submodule.ext` `RingHomCompTriple.ids` `Submodule.coe_mem`
`ker_linearProjOfIsCompl` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `IsCompl` `Submodule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `range` `RingHomSurjective.ids`	`ker` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `linearProjOfIsCompl`	—	`RingHomSurjective.ids` `LinearEquiv.ker_comp` `Submodule.linearProjOfIsCompl_ker`
`linearProjOfIsCompl_apply_left` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `IsCompl` `Submodule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `range` `RingHomSurjective.ids`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `linearProjOfIsCompl`	—	`RingHomSurjective.ids` `RingHomSurjective.invPair` `RingHomInvPair.ids` `LinearEquiv.surjective` `LinearEquiv.ofInjective_symm_apply` `Submodule.linearProjOfIsCompl_apply_left`
`linearProjOfIsCompl_apply_right` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `IsCompl` `Submodule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `range` `RingHomSurjective.ids`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `linearProjOfIsCompl` `Submodule` `SetLike.instMembership` `Submodule.setLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomSurjective.ids` `Submodule.linearProjOfIsCompl_apply_right` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`linearProjOfIsCompl_apply_right'` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `IsCompl` `Submodule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `range` `RingHomSurjective.ids` `SetLike.instMembership` `Submodule.setLike`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `linearProjOfIsCompl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomSurjective.ids` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`linearProjOfIsCompl_of_proj` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instFunLike`	`Submodule.linearProjOfIsCompl` `ker` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `isCompl_of_proj`	—	`ext` `isCompl_of_proj` `IsCompl.sup_eq_top` `Submodule.mem_sup'` `map_add` `SemilinearMapClass.toAddHomClass` `semilinearMapClass` `Submodule.linearProjOfIsCompl_apply_left` `Submodule.linearProjOfIsCompl_apply_right` `add_zero` `map_coe_ker`
`ofIsComplProd_apply` 📖	mathematical	`IsCompl` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instFunLike` `ofIsComplProd` `ofIsCompl`	—	`smulCommClass_self`
`ofIsCompl_add` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`ofIsCompl` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instAdd`	—	`ofIsCompl_eq` `ofIsCompl_left_apply` `ofIsCompl_right_apply`
`ofIsCompl_eq` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instFunLike`	`ofIsCompl`	—	`ext` `Submodule.existsUnique_add_of_isCompl` `RingHomCompTriple.ids` `IsCompl.symm` `comp.congr_simp` `Submodule.toLinearMap_prodEquivOfIsCompl_symm` `map_add` `SemilinearMapClass.toAddHomClass` `semilinearMapClass` `Submodule.linearProjOfIsCompl_apply_left` `Submodule.linearProjOfIsCompl_apply_right` `add_zero` `zero_add`
`ofIsCompl_eq'` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `comp` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Submodule.subtype`	`ofIsCompl`	—	`RingHomCompTriple.ids` `ofIsCompl_eq`
`ofIsCompl_eq_add` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`ofIsCompl` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instAdd` `comp` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHomCompTriple.ids` `Submodule.linearProjOfIsCompl` `IsCompl.symm` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	`ext` `RingHomCompTriple.ids` `IsCompl.symm` `Submodule.existsUnique_add_of_isCompl` `map_add` `SemilinearMapClass.toAddHomClass` `semilinearMapClass` `ofIsCompl_left_apply` `ofIsCompl_right_apply` `Submodule.linearProjOfIsCompl_apply_left` `Submodule.linearProjOfIsCompl_apply_right` `add_zero` `zero_add`
`ofIsCompl_left_apply` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `ofIsCompl` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomCompTriple.ids` `IsCompl.symm` `comp.congr_simp` `Submodule.toLinearMap_prodEquivOfIsCompl_symm` `Submodule.linearProjOfIsCompl_apply_left` `Submodule.linearProjOfIsCompl_apply_right` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `add_zero`
`ofIsCompl_right_apply` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `ofIsCompl` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomCompTriple.ids` `IsCompl.symm` `comp.congr_simp` `Submodule.toLinearMap_prodEquivOfIsCompl_symm` `Submodule.linearProjOfIsCompl_apply_right` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `Submodule.linearProjOfIsCompl_apply_left` `zero_add`
`ofIsCompl_smul` 📖	mathematical	`IsCompl` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`ofIsCompl` `CommRing.toRing` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring`	—	`ofIsCompl_eq` `smulCommClass_self` `ofIsCompl_left_apply` `ofIsCompl_right_apply`
`ofIsCompl_subtype_zero_eq` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`ofIsCompl` `Submodule.subtype` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instZero` `Submodule.IsCompl.projection`	—	`RingHomCompTriple.ids` `IsCompl.symm` `ofIsCompl_eq_add` `add_zero`
`ofIsCompl_symm` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`ofIsCompl` `IsCompl.symm` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	`IsCompl.symm` `RingHomCompTriple.ids` `ofIsCompl_eq_add` `add_comm`
`ofIsCompl_zero` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`ofIsCompl` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instZero`	—	`ofIsCompl_eq`
`range_eq_of_proj` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instFunLike`	`range` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Top.top` `Submodule.instTop`	—	`RingHomSurjective.ids` `range_eq_top`
`range_ofIsCompl` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ofIsCompl` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `IsCompl.symm` `ofIsCompl_eq_add` `le_antisymm` `LE.le.trans` `range_add_le` `sup_le_sup` `range_comp_le_range` `sup_le` `Submodule.linearProjOfIsCompl_apply_left` `Submodule.linearProjOfIsCompl_apply_right` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `add_zero` `zero_add`
`surjective_comp_linearProjOfIsCompl` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `comp` `RingHomCompTriple.ids` `Submodule.linearProjOfIsCompl`	—	`RingHomCompTriple.ids` `ext` `Submodule.linearProjOfIsCompl_apply_left`
`surjective_comp_subtype_of_isComplemented` 📖	mathematical	`IsComplemented` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `CompleteLattice.toBoundedOrder`	`LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `comp` `RingHomCompTriple.ids` `Submodule.subtype`	—	`RingHomCompTriple.ids` `ext` `Submodule.linearProjOfIsCompl_apply_left`

LinearMap.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_iff` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`Commute` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `Submodule` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearMap.range` `RingHomSurjective.ids` `LinearMap.ker`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `range_mem_invtSubmodule_iff` `ker_mem_invtSubmodule_iff` `Commute.eq` `IsIdempotentElem.eq`
`commute_iff_of_isUnit` 📖	mathematical	`IsUnit` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMonoid` `IsIdempotentElem` `Module.End.instMul`	`Commute` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `Submodule.map` `RingHomSurjective.ids` `LinearMap.range` `LinearMap.ker`	—	`RingHomSurjective.ids` `CanLift.prf` `instCanLiftUnitsValIsUnit` `RingHomInvPair.ids` `Submodule.map.congr_simp` `commute_iff` `LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap` `Commute.units_inv_right`
`comp_eq_left_iff` 📖	mathematical	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`LinearMap.comp` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.ker`	—	`RingHomCompTriple.ids` `RingHomSurjective.ids` `ker_eq_range` `LinearMap.comp_sub`
`comp_eq_right_iff` 📖	mathematical	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End.instMul`	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.range` `RingHomSurjective.ids`	—	`RingHomCompTriple.ids` `RingHomSurjective.ids` `mem_range_iff` `instIsConcreteLE`
`conj_eq_of_ker_mem_invtSubmodule` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `Submodule` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearMap.ker`	`LinearMap.comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `ker_mem_invtSubmodule_iff`
`conj_eq_of_range_mem_invtSubmodule` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `Submodule` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearMap.range` `RingHomSurjective.ids`	`LinearMap.comp` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `range_mem_invtSubmodule_iff`
`eq_isCompl_projection` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`Submodule.IsCompl.projection` `LinearMap.range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.ker` `isCompl`	—	`RingHomSurjective.ids` `isCompl` `LinearMap.ofIsCompl_eq` `LinearMap.IsProj.map_id` `isProj_range` `LinearMap.map_coe_ker` `LinearMap.ofIsCompl_subtype_zero_eq`
`ext` 📖	—	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `LinearMap.range` `RingHomSurjective.ids` `LinearMap.ker`	—	—	`RingHomSurjective.ids` `ext_iff`
`ext_iff` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`LinearMap.range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.ker`	—	`RingHomSurjective.ids` `LinearMap.ext` `Submodule.existsUnique_add_of_isCompl` `IsCompl.symm` `isCompl` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `LinearMap.mem_ker` `mem_range_iff` `zero_add`
`isCompl` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.ker`	—	`LinearMap.IsProj.isCompl` `RingHomSurjective.ids` `isProj_range`
`isProj_range` 📖	mathematical	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End.instMul`	`LinearMap.IsProj` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap` `LinearMap.instFunLike`	—	`RingHomSurjective.ids` `LinearMap.isProj_range_iff_isIdempotentElem`
`ker_eq_range` 📖	mathematical	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`LinearMap.ker` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.range` `RingHomSurjective.ids` `LinearMap` `LinearMap.instSub` `LinearMap.id`	—	`RingHomSurjective.ids` `sub_sub_cancel` `range_eq_ker_one_sub` `IsIdempotentElem.one_sub`
`ker_eq_range_one_sub` 📖	mathematical	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`LinearMap.ker` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.range` `RingHomSurjective.ids` `LinearMap` `LinearMap.instSub` `Module.End.instOne`	—	`ker_eq_range`
`ker_mem_invtSubmodule` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `LinearMap.comp` `RingHomCompTriple.ids`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`RingHomCompTriple.ids` `ker_mem_invtSubmodule_iff`
`ker_mem_invtSubmodule_iff` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `LinearMap.comp_assoc` `comp_eq_left_iff` `LinearMap.ker_comp` `Module.End.mem_invtSubmodule`
`mem_range_iff` 📖	mathematical	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End.instMul`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`LinearMap.IsProj.mem_iff_map_id` `RingHomSurjective.ids` `isProj_range`
`range_eq_ker` 📖	mathematical	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`LinearMap.range` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.ker` `LinearMap` `LinearMap.instSub` `LinearMap.id`	—	`le_antisymm` `RingHomSurjective.ids` `LinearMap.range_le_ker_iff` `IsIdempotentElem.one_sub_mul_self`
`range_eq_ker_one_sub` 📖	mathematical	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`LinearMap.range` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.ker` `LinearMap` `LinearMap.instSub` `Module.End.instOne`	—	`range_eq_ker`
`range_mem_invtSubmodule` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `LinearMap.comp` `RingHomCompTriple.ids`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `range_mem_invtSubmodule_iff`
`range_mem_invtSubmodule_iff` 📖	mathematical	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `comp_eq_right_iff` `LinearMap.range_comp` `Module.End.mem_invtSubmodule_iff_map_le`

LinearMap.IsProj

Definitions

Name	Category	Theorems
`codRestrict` 📖	CompOp	4 math math: `subtype_comp_codRestrict`, `codRestrict_apply_cod`, `codRestrict_ker`, `codRestrict_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot` 📖	mathematical	—	`LinearMap.IsProj` `Bot.bot` `Submodule` `Submodule.instBot` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `LinearMap.instZero`	—	—
`codRestrict_apply` 📖	mathematical	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `codRestrict`	—	`LinearMap.codRestrict_apply`
`codRestrict_apply_cod` 📖	mathematical	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `codRestrict`	—	`codRestrict_apply` `map_id`
`codRestrict_ker` 📖	mathematical	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearMap.ker` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `codRestrict`	—	`LinearMap.ker_codRestrict`
`eq_conj_prodMap` 📖	mathematical	`LinearMap.IsProj` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `RingHomInvPair.ids` `Module.End` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearMap.ker` `Prod.instAddCommMonoid` `Submodule.addCommMonoid` `Prod.instModule` `Submodule.module` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.conj` `Submodule.prodEquivOfIsCompl` `isCompl` `LinearMap.prodMap` `LinearMap.id` `LinearMap` `LinearMap.instZero`	—	`RingHomInvPair.ids` `smulCommClass_self` `isCompl` `RingHomInvPair.triples₂` `RingHomCompTriple.ids` `LinearEquiv.conj_apply` `eq_conj_prod_map'`
`eq_conj_prod_map'` 📖	mathematical	`LinearMap.IsProj` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearMap.comp` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Submodule.addCommMonoid` `Prod.instModule` `Submodule.module` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `Submodule.prodEquivOfIsCompl` `isCompl` `LinearMap.prodMap` `LinearMap.id` `LinearMap` `LinearMap.instZero` `LinearEquiv.symm`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `isCompl` `LinearMap.comp_assoc` `LinearEquiv.eq_comp_toLinearMap_symm` `LinearMap.prod_ext` `LinearMap.ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_zero` `map_id` `zero_add` `LinearMap.map_coe_ker`
`isCompl` 📖	mathematical	`LinearMap.IsProj` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`codRestrict_ker` `LinearMap.isCompl_of_proj` `codRestrict_apply_cod`
`isIdempotentElem` 📖	mathematical	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End.instMul`	—	`LinearMap.isProj_iff_isIdempotentElem`
`map_id` 📖	mathematical	`LinearMap.IsProj` `Submodule` `SetLike.instMembership` `Submodule.setLike`	`DFunLike.coe`	—	—
`map_mem` 📖	mathematical	`LinearMap.IsProj`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe`	—	—
`mem_iff_map_id` 📖	mathematical	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`map_id` `map_mem`
`mem_invtSubmodule_iff` 📖	mathematical	`LinearMap.IsProj` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule` `LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff` `isIdempotentElem` `range`
`range` 📖	mathematical	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids`	—	`submodule_unique` `RingHomSurjective.ids` `LinearMap.IsIdempotentElem.isProj_range` `isIdempotentElem`
`submodule_eq_bot_iff` 📖	mathematical	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Bot.bot` `Submodule` `Submodule.instBot` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instZero`	—	`LinearMap.ext` `map_mem` `RingHomSurjective.ids` `range` `LinearMap.range_zero`
`submodule_eq_top_iff` 📖	mathematical	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Top.top` `Submodule` `Submodule.instTop` `LinearMap.id`	—	`LinearMap.ext` `map_id` `RingHomSurjective.ids` `range` `LinearMap.range_id`
`submodule_unique` 📖	—	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	—	`Submodule.ext` `mem_iff_map_id`
`subtype_comp_codRestrict` 📖	mathematical	`LinearMap.IsProj` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LinearMap.comp` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Submodule.subtype` `codRestrict`	—	`RingHomCompTriple.ids`
`top` 📖	mathematical	—	`LinearMap.IsProj` `Top.top` `Submodule` `Submodule.instTop` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `LinearMap.id`	—	—

Submodule

Definitions

Name	Category	Theorems
`isComplEquivProj` 📖	CompOp	2 math math: `coe_isComplEquivProj_symm_apply`, `coe_isComplEquivProj_apply`
`isIdempotentElemEquiv` 📖	CompOp	2 math math: `isIdempotentElemEquiv_apply_coe`, `isIdempotentElemEquiv_symm_apply_coe`
`linearProjOfIsCompl` 📖	CompOp	25 math math: `coe_continuous_linearProjOfClosedCompl'`, `linearProjOfIsCompl_apply_left`, `linearProjOfIsCompl_apply_right`, `linearProjOfIsCompl_comp_surjective_of_exact`, `linearProjOfIsCompl_apply_right'`, `coe_linearProjOfIsCompl_apply`, `coe_continuous_linearProjOfClosedCompl`, `prodEquivOfIsCompl_symm_apply`, `orthogonalProjection_apply_eq_linearProjOfIsCompl`, `coe_isComplEquivProj_apply`, `linearProjOfIsCompl_isCompl_projection`, `linearProjOfIsCompl_comp_subtype`, `toLinearMap_prodEquivOfIsCompl_symm`, `toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl`, `IsCompl.projection_apply`, `LinearMap.surjective_comp_linearProjOfIsCompl`, `linearProjOfIsCompl_comp_bijective_of_exact`, `linearProjOfIsCompl_range`, `LinearMap.linearProjOfIsCompl_of_proj`, `linearProjOfIsCompl_ker`, `linearProjOfIsCompl_apply_eq_zero_iff`, `linearProjOfIsCompl_surjective`, `orthogonalProjection_coe_eq_linearProjOfIsCompl`, `orthogonalProjection_eq_linearProjOfIsCompl`, `LinearMap.ofIsCompl_eq_add`
`prodEquivOfIsCompl` 📖	CompOp	15 math math: `toLinearEquiv_orthogonalDecomposition_symm`, `prodEquivOfIsCompl_symm_apply_snd_eq_zero`, `toLinearEquiv_orthogonalDecomposition`, `coe_prodEquivOfIsCompl'`, `LinearMap.IsProj.eq_conj_prodMap`, `coe_prodEquivOfIsCompl`, `prodEquivOfIsCompl_symm_apply_fst_eq_zero`, `prodEquivOfIsCompl_symm_apply`, `prodComm_trans_prodEquivOfIsCompl`, `prodEquivOfIsCompl_symm_apply_left`, `toLinearMap_prodEquivOfIsCompl_symm`, `LinearMap.IsProj.eq_conj_prod_map'`, `prodEquivOfIsCompl_symm_apply_right`, `coe_prodEquivOfClosedCompl`, `coe_prodEquivOfClosedCompl_symm`
`quotientEquivOfIsCompl` 📖	CompOp	3 math math: `quotientEquivOfIsCompl_apply_mk_coe`, `quotientEquivOfIsCompl_symm_apply`, `mk_quotientEquivOfIsCompl_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_isComplEquivProj_apply` 📖	mathematical	—	`LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `DFunLike.coe` `Equiv` `IsCompl` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice` `EquivLike.toFunLike` `Equiv.instEquivLike` `isComplEquivProj` `linearProjOfIsCompl`	—	—
`coe_isComplEquivProj_symm_apply` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `IsCompl` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice` `DFunLike.coe` `Equiv` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `isComplEquivProj` `LinearMap.ker`	—	—
`coe_linearProjOfIsCompl_apply` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `LinearMap.instFunLike` `linearProjOfIsCompl` `IsCompl.projection`	—	—
`coe_prodEquivOfIsCompl` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `prodEquivOfIsCompl` `LinearMap.coprod` `subtype`	—	`RingHomInvPair.ids`
`coe_prodEquivOfIsCompl'` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `prodEquivOfIsCompl` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`RingHomInvPair.ids`
`existsUnique_add_of_isCompl` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`existsUnique_add_of_isCompl_prod` `Prod.eq_iff_fst_eq_snd_eq`
`existsUnique_add_of_isCompl_prod` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`ExistsUnique` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Function.Bijective.existsUnique` `RingHomInvPair.ids` `Equiv.bijective`
`isIdempotentElemEquiv_apply_coe` 📖	mathematical	—	`LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `DFunLike.coe` `Equiv` `Module.End` `IsIdempotentElem` `Module.End.instMul` `LinearMap.range` `RingHomSurjective.ids` `EquivLike.toFunLike` `Equiv.instEquivLike` `isIdempotentElemEquiv` `LinearMap.codRestrict`	—	`RingHomSurjective.ids`
`isIdempotentElemEquiv_symm_apply_coe` 📖	mathematical	—	`Module.End` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `IsIdempotentElem` `Module.End.instMul` `Submodule` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `Equiv` `LinearMap` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `RingHomSurjective.ids` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `isIdempotentElemEquiv` `LinearMap.comp` `subtype`	—	`RingHomSurjective.ids`
`linearProjOfIsCompl_apply_eq_zero_iff` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `LinearMap.instFunLike` `linearProjOfIsCompl` `zero`	—	—
`linearProjOfIsCompl_apply_left` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `LinearMap.instFunLike` `linearProjOfIsCompl`	—	`prodEquivOfIsCompl_symm_apply_left`
`linearProjOfIsCompl_apply_right` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `LinearMap.instFunLike` `linearProjOfIsCompl` `zero`	—	`linearProjOfIsCompl_apply_right'`
`linearProjOfIsCompl_apply_right'` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice` `SetLike.instMembership` `setLike`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `LinearMap.instFunLike` `linearProjOfIsCompl` `zero`	—	`linearProjOfIsCompl_apply_eq_zero_iff`
`linearProjOfIsCompl_comp_subtype` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`LinearMap.comp` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `linearProjOfIsCompl` `subtype` `LinearMap.id`	—	`LinearMap.ext` `RingHomCompTriple.ids` `linearProjOfIsCompl_apply_left`
`linearProjOfIsCompl_isCompl_projection` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `LinearMap.instFunLike` `linearProjOfIsCompl` `IsCompl.projection`	—	`linearProjOfIsCompl_apply_left`
`linearProjOfIsCompl_ker` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`LinearMap.ker` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `linearProjOfIsCompl`	—	`ext` `LinearMap.mem_ker` `linearProjOfIsCompl_apply_eq_zero_iff`
`linearProjOfIsCompl_range` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`LinearMap.range` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `linearProjOfIsCompl` `Top.top` `instTop`	—	`LinearMap.range_eq_of_proj` `linearProjOfIsCompl_apply_left`
`linearProjOfIsCompl_surjective` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `LinearMap.instFunLike` `linearProjOfIsCompl`	—	`RingHomSurjective.ids` `LinearMap.range_eq_top` `linearProjOfIsCompl_range`
`mk_quotientEquivOfIsCompl_apply` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `HasQuotient.Quotient` `hasQuotient` `Quotient.addCommGroup` `addCommMonoid` `Quotient.module` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `quotientEquivOfIsCompl`	—	`LinearEquiv.symm_apply_apply` `RingHomInvPair.ids`
`prodComm_trans_prodEquivOfIsCompl` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`LinearEquiv.trans` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.prodComm` `prodEquivOfIsCompl` `IsCompl.symm` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	—	`LinearEquiv.ext` `RingHomInvPair.ids` `RingHomCompTriple.ids` `IsCompl.symm` `add_comm`
`prodEquivOfIsCompl_symm_apply` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `prodEquivOfIsCompl` `LinearMap` `LinearMap.instFunLike` `linearProjOfIsCompl` `IsCompl.symm` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	—	`RingHomInvPair.ids` `IsCompl.symm` `RingHomCompTriple.ids` `prodComm_trans_prodEquivOfIsCompl`
`prodEquivOfIsCompl_symm_apply_fst_eq_zero` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `prodEquivOfIsCompl` `zero`	—	`RingHomInvPair.ids` `LinearEquiv.apply_symm_apply` `coe_prodEquivOfIsCompl'` `add_mem_iff_left` `coe_mem` `mem_right_iff_eq_zero_of_disjoint` `IsCompl.disjoint`
`prodEquivOfIsCompl_symm_apply_left` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `prodEquivOfIsCompl` `zero`	—	`RingHomInvPair.ids` `LinearEquiv.symm_apply_eq` `add_zero`
`prodEquivOfIsCompl_symm_apply_right` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `prodEquivOfIsCompl` `zero`	—	`RingHomInvPair.ids` `LinearEquiv.symm_apply_eq` `zero_add`
`prodEquivOfIsCompl_symm_apply_snd_eq_zero` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `prodEquivOfIsCompl` `zero`	—	`RingHomInvPair.ids` `LinearEquiv.apply_symm_apply` `coe_prodEquivOfIsCompl'` `add_mem_iff_right` `coe_mem` `mem_left_iff_eq_zero_of_disjoint` `IsCompl.disjoint`
`quotientEquivOfIsCompl_apply_mk_coe` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `hasQuotient` `SetLike.instMembership` `setLike` `Quotient.addCommGroup` `addCommMonoid` `Quotient.module` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `quotientEquivOfIsCompl`	—	`LinearEquiv.apply_symm_apply` `RingHomInvPair.ids`
`quotientEquivOfIsCompl_symm_apply` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `HasQuotient.Quotient` `hasQuotient` `addCommMonoid` `Quotient.addCommGroup` `module` `Quotient.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `quotientEquivOfIsCompl`	—	`RingHomInvPair.ids`
`toLinearMap_prodEquivOfIsCompl_symm` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	`LinearEquiv.toLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `LinearEquiv.symm` `prodEquivOfIsCompl` `LinearMap.prod` `linearProjOfIsCompl` `IsCompl.symm` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice`	—	`LinearMap.ext` `RingHomInvPair.ids` `IsCompl.symm` `prodEquivOfIsCompl_symm_apply`

Submodule.IsCompl

Definitions

Name	Category	Theorems
`projection` 📖	CompOp	21 math math: `Submodule.starProjection_apply_eq_isComplProjection`, `projection_isSymmetricProjection_iff`, `projection_apply_left`, `LinearMap.isIdempotentElem_iff_eq_isCompl_projection_range_ker`, `LinearMap.IsIdempotentElem.eq_isCompl_projection`, `Submodule.coe_linearProjOfIsCompl_apply`, `projection_isSymmetricProjection_of_isOrtho`, `Submodule.toLinearMap_starProjection_eq_isComplProjection`, `projection_eq_self_iff`, `Submodule.linearProjOfIsCompl_isCompl_projection`, `projection_add_projection_eq_self`, `projection_ker`, `projection_apply_eq_zero_iff`, `projection_apply`, `projection_range`, `projection_eq_self_sub_projection`, `LinearMap.ofIsCompl_subtype_zero_eq`, `projection_isIdempotentElem`, `projection_apply_mem`, `Submodule.starProjection_coe_eq_isCompl_projection`, `projection_isSymmetric_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`projection_add_projection_eq_self` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `projection` `IsCompl.symm` `Submodule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	`IsCompl.symm` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Submodule.prodComm_trans_prodEquivOfIsCompl` `LinearEquiv.apply_symm_apply`
`projection_apply` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `projection` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Submodule.linearProjOfIsCompl`	—	—
`projection_apply_eq_zero_iff` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `projection` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike`	—	`AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`projection_apply_left` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `projection` `Submodule` `SetLike.instMembership` `Submodule.setLike`	—	`Submodule.linearProjOfIsCompl_apply_left`
`projection_apply_mem` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `projection`	—	`SetLike.coe_mem`
`projection_eq_self_iff` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `projection` `Submodule` `SetLike.instMembership` `Submodule.setLike`	—	`sub_eq_zero` `IsCompl.symm` `projection_eq_self_sub_projection` `projection_apply_eq_zero_iff`
`projection_eq_self_sub_projection` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `projection` `IsCompl.symm` `Submodule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsCompl.symm` `eq_sub_iff_add_eq` `projection_add_projection_eq_self`
`projection_isIdempotentElem` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`IsIdempotentElem` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `projection`	—	`LinearMap.ext` `Submodule.linearProjOfIsCompl_isCompl_projection`
`projection_ker` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`LinearMap.ker` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `projection`	—	`Submodule.ker_subtype` `Submodule.linearProjOfIsCompl_ker`
`projection_range` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`LinearMap.range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `projection`	—	`RingHomSurjective.ids` `LinearMap.range_comp` `Submodule.map.congr_simp` `Submodule.linearProjOfIsCompl_range` `Submodule.map_top` `Submodule.range_subtype`

---

← Back to Index