Theorems · Definition · linear algebra

LinearMap.lcomp

{R : Type u_1} →
  (S : Type u_3) →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {M : Type u_5} →
          {M₂ : Type u_6} →
            (N : Type u_7) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module S N] →
                          [inst_8 : Module R N] →
                            [inst_9 : SMulCommClass R S N] → (M →ₗ[R] M₂) → (M₂ →ₗ[R] N) →ₗ[S] M →ₗ[R] N

Composing a given linear map M → N with a linear map N → P as a linear map from Nₗ →ₗ[R] Pₗ to M →ₗ[R] Pₗ.

Defined in

Mathlib.LinearAlgebra.BilinearMap

Cited by

16 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Quot.sound

Assumes

SemiringSemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleSMulCommClass