Theorems · Definition · category theory

CategoryTheory.Linear.comp

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : Type w} →
        [inst_2 : CommSemiring S] →
          [inst_3 : CategoryTheory.Linear S C] → (X Y Z : C) → (X ⟶ Y) →ₗ[S] (Y ⟶ Z) →ₗ[S] X ⟶ Z

Composition as a bilinear map.

Defined in: Mathlib.CategoryTheory.Linear.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 33 from the axioms · uses propext, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Preadditive CommSemiring CategoryTheory.Linear

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
RingHom.idstatement · cited by 18,349
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement · cited by 10,215
CategoryTheory.Preadditivestatement and proof · cited by 3,309
CategoryTheory.Linearstatement and proof · cited by 131
CategoryTheory.Linear.leftCompproof · cited by 7

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.Linear.comp_applystatement and proof · cited by 0