Theorems · Definition · linear algebra

LinearMap.pi

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

pi construction for linear functions. From a family of linear functions it produces a linear function into a family of modules.

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

31 results in Mathlib

Foundations

Depth 24 from the axioms · uses Quot.sound

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule