Commit 2023-03-09 14:54 b50d5f48

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Linear/Basic.lean

added def CategoryTheory.Linear.comp

added def CategoryTheory.Linear.leftComp

added def CategoryTheory.Linear.rightComp