Def CategoryTheory.WithInitial.mkCommaMorphism

Modification history

2025-04-30 12:59
Mathlib/CategoryTheory/WithTerminal/Basic.lean
style: further whitespace fixes (#24467) …
Modified CategoryTheory.WithInitial.mkCommaMorphismView on Github →
2025-03-13 09:34
Mathlib/CategoryTheory/WithTerminal.lean
feat(CategoryTheory/WithTerminal): functors out of `WithTerminal` (#22658) …
Added CategoryTheory.WithInitial.mkCommaMorphismView on Github →