Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.Mat.id_apply

Modification history

2022-03-12 18:01

src/category_theory/preadditive/Mat.lean

feat(category_theory/preadditive/Mat): ring version (#12617)

Added category_theory.Mat.id_apply View on Github →