Theorems · Theorem · category theory

CoalgCat.whiskerLeft_def

∀ (R : Type u) [inst : CommRing R] (X x x_1 : CoalgCat R) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f =
    CoalgCat.ofHom (CoalgHom.lTensor (↑X.toModuleCat) f.toCoalgHom')

Defined in: Mathlib.Algebra.Category.CoalgCat.Monoidal
Cited by: 0 results in Mathlib
Foundations: Depth 82 from the axioms · uses propext, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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

Quiver.Homstatement and proof · cited by 32,603
CommRingstatement and proof · cited by 17,173
TensorProductstatement · cited by 2,545
ModuleCat.carrierstatement · cited by 997
CategoryTheory.MonoidalCategoryStruct.whiskerLeftstatement and proof · cited by 915
CoalgCatstatement and proof · cited by 63
CoalgCat.toModuleCatstatement · cited by 51
CoalgCat.ofstatement · cited by 24
CoalgCat.Hom.toCoalgHom'statement · cited by 11
CoalgCat.ofHomstatement · cited by 7
CoalgHom.lTensorstatement · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.