Def CategoryTheory.Linear.comp

Modification history

2024-05-17 19:31

Mathlib/CategoryTheory/Linear/Basic.lean

style: remove all isolated `where` (#12991)

Modified CategoryTheory.Linear.comp View on Github →

2023-03-09 14:54

Mathlib/CategoryTheory/Linear/Basic.lean

feat: port CategoryTheory.Linear.Basic (#2744)

Added CategoryTheory.Linear.comp View on Github →