Theorem CategoryTheory.RelCat.Hom.rel_id_apply₂

Modification history

2025-07-06 13:16
Mathlib/CategoryTheory/Category/RelCat.lean
refactor: make `Rel` less see-through (#25587) …
Modified CategoryTheory.RelCat.Hom.rel_id_apply₂View on Github →
2025-06-15 11:36
Mathlib/CategoryTheory/Category/RelCat.lean
refactor(RelCat): use a type synonym for homs (#25593) …
Modified CategoryTheory.RelCat.Hom.rel_id_apply₂View on Github →
2024-04-29 12:02
Mathlib/CategoryTheory/Category/RelCat.lean
feat(CategoryTheory/Category/RelCat): Show basic facts and self-duality of category of relations. (#11241) …
Added CategoryTheory.RelCat.Hom.rel_id_apply₂View on Github →