Theorems · Definition · linear algebra

LinearMap.proj

{R : Type u} →
  {ι : Type x} →
    [inst : Semiring R] →
      {φ : ι → Type i} →
        [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
          [inst_2 : (i : ι) → Module R (φ i)] → (i : ι) → ((i : ι) → φ i) →ₗ[R] φ i

The projections from a family of modules are linear maps. Note: this definition would be called Pi.evalLinearMap if we followed the pattern established by Pi.evalAddHom, Pi.evalMonoidHom, Pi.evalRingHom, ...

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

71 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

SemiringAddCommMonoidModule