Theorems · Definition · ring theory

LinearMap.comp

{R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {R₃ : Type u_4} →
      {M₁ : Type u_9} →
        {M₂ : Type u_10} →
          {M₃ : Type u_11} →
            [inst : Semiring R₁] →
              [inst_1 : Semiring R₂] →
                [inst_2 : Semiring R₃] →
                  [inst_3 : AddCommMonoid M₁] →
                    [inst_4 : AddCommMonoid M₂] →
                      [inst_5 : AddCommMonoid M₃] →
                        {module_M₁ : Module R₁ M₁} →
                          {module_M₂ : Module R₂ M₂} →
                            {module_M₃ : Module R₃ M₃} →
                              {σ₁₂ : R₁ →+* R₂} →
                                {σ₂₃ : R₂ →+* R₃} →
                                  {σ₁₃ : R₁ →+* R₃} →
                                    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                      (M₂ →ₛₗ[σ₂₃] M₃) → (M₁ →ₛₗ[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₃] M₃

Composition of two linear maps is a linear map

Defined in

Mathlib.Algebra.Module.LinearMap.Defs

Cited by

1,642 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 198 definitions · uses propext, Quot.sound

Assumes

SemiringSemiringSemiringAddCommMonoidAddCommMonoidAddCommMonoidRingHomCompTriple