Theorems · Definition · linear algebra

Submodule.projectionOnto

{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] ↥p

Projection to a submodule along a complement. It is the unique linear map f : E → p such that f x = x for x ∈ p and f x = 0 for x ∈ q. For the projection from E to E, see Submodule.projection. See also: * Submodule.projectionOntoL and Submodule.projectionL for the continuous versions. * Submodule.orthogonalProjection and Submodule.orthogonalProjectionOnto for the projections along the orthogonal subspace. See also LinearMap.linearProjOfIsCompl.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

81 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule