Theorems · Theorem · commutative algebra

RingCat.comp_apply

∀ {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) r =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) r)

Defined in: Mathlib.Algebra.Category.Ring.Basic
Cited by: 4 results in Mathlib
Foundations: Depth 24 from the axioms · uses propext, Quot.sound

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.

DFunLike.coestatement and proof · cited by 62,936
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.CategoryStruct.compstatement · cited by 17,999
RingHomstatement · cited by 10,189
CategoryTheory.ConcreteCategory.homstatement · cited by 4,022
RingCatstatement and proof · cited by 473
RingCat.carrierstatement and proof · cited by 279
RingCat.Hom.homproof · cited by 85

Cited by4

Results whose statement or proof uses this declaration.

CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_auxproof · cited by 1
PresheafOfModules.Sheafify.map_smulproof · cited by 0
CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smulproof · cited by 0
RingCat.Colimits.cocone_naturality_componentsproof · cited by 0