Theorems · Inductive type · linear algebra

LinearMap.IsProj

{S : Type u_5} →
  [inst : Semiring S] →
    {M : Type u_6} →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module S M] → Submodule S M → {F : Type u_7} → [FunLike F M M] → F → Prop

A linear endomorphism of a module E is a projection onto a submodule p if it sends every element of E to p and fixes every element of p. The definition allow more generally any FunLike type and not just linear maps, so that it can be used for example with ContinuousLinearMap or Matrix.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

23 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

SemiringAddCommMonoidModuleFunLike