Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.End.smul_right

Modification history

2022-01-31 14:14

src/category_theory/endomorphism.lean

feat(category_theory/preadditive): the Yoneda embedding for preadditive categories (#11740)

Added category_theory.End.smul_right View on Github →