Commit 2024-08-12 17:47 c3a48aba

View on Github →

feat(CategoryTheory): Composing Comma.map with Comma.fst and Comma.snd (#15730)

Estimated changes

Modified Mathlib/CategoryTheory/Comma/Basic.lean

added def CategoryTheory.Comma.mapFst

added def CategoryTheory.Comma.mapSnd

added theorem CategoryTheory.Comma.map_fst

added theorem CategoryTheory.Comma.map_snd