Def CategoryTheory.Quotient.Linear.smul

Modification history

2024-07-28 23:33

Mathlib/CategoryTheory/Quotient/Linear.lean

chore: robustifying for debug.byAsSorry (part 13) (#15197)

Modified CategoryTheory.Quotient.Linear.smul View on Github →

2024-02-25 22:07

Mathlib/CategoryTheory/Quotient/Linear.lean

feat(CategoryTheory): the quotient category is linear (#10887) …

Added CategoryTheory.Quotient.Linear.smul View on Github →