Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-03 10:20 e39f617c

View on Github →

feat(category_theory/linear): compatibility of linear Yoneda (#11784)

Estimated changes

Modified src/category_theory/linear/yoneda.lean

added def category_theory.linear_coyoneda

added theorem category_theory.whiskering_linear_coyoneda

added theorem category_theory.whiskering_linear_coyoneda₂

added theorem category_theory.whiskering_linear_yoneda

added theorem category_theory.whiskering_linear_yoneda₂