Theorem Prefunctor.id_comp

Modification history

2023-08-10 19:52

Mathlib/Combinatorics/Quiver/Basic.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Prefunctor.id_comp View on Github →

2022-12-05 07:41

Mathlib/Combinatorics/Quiver/Basic.lean

feat(Combinatorics/Quiver/Basic): Add comp_id and id_comp lemmas for prefunctors (#858) …

Added Prefunctor.id_comp View on Github →