Theorems · Definition · linear algebra

LinearMap.llcomp

{R : Type u_2} →
  [inst : CommSemiring R] →
    {R₂ : Type u_14} →
      (R₃ : Type u_15) →
        (M : Type u_17) →
          (N : Type u_18) →
            (P : Type u_19) →
              [inst_1 : CommSemiring R₂] →
                [inst_2 : CommSemiring R₃] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : AddCommMonoid N] →
                      [inst_5 : AddCommMonoid P] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module R₂ N] →
                            [inst_8 : Module R₃ P] →
                              {σ₁₂ : R →+* R₂} →
                                {σ₁₃ : R →+* R₃} →
                                  {σ₂₃ : R₂ →+* R₃} →
                                    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                      (N →ₛₗ[σ₂₃] P) →ₗ[R₃] (M →ₛₗ[σ₁₂] N) →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P

Composing linear maps as a bilinear map from (M →ₛₗ[σ₁₂] N) × (N →ₛₗ[σ₂₃] P) to M →ₛₗ[σ₁₃] P.

Defined in

Mathlib.LinearAlgebra.BilinearMap

Cited by

15 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleRingHomCompTriple