Theorems · Definition · linear algebra

Submodule.projection

{R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} → [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → (p q : Submodule R E) → IsCompl p q → E →ₗ[R] E

The linear projection onto a subspace along its complement as a map from the full space to itself, as opposed to Submodule.projectionOnto, which maps into the subtype. This version is important as it satisfies IsIdempotentElem. See also: * Submodule.projectionOntoL and Submodule.projectionL for the continuous versions. * Submodule.orthogonalProjection and Submodule.orthogonalProjectionOnto for the projections along the orthogonal subspace.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

63 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModule