Theorem CategoryTheory.Comma.inv_right

Modification history

2026-06-16 12:08

Mathlib/CategoryTheory/Comma/Basic.lean

feat(CategoryTheory/Comma/Basic): use `to_dual` more (#40355) …

Deleted CategoryTheory.Comma.inv_right View on Github →

2024-10-24 04:49

Mathlib/CategoryTheory/Comma/Basic.lean

feat(CategoryTheory/Comma): subcategory defined by morphism properties (#18088) …

Added CategoryTheory.Comma.inv_right View on Github →