Commit 2025-02-26 22:41 6b00c05d

View on Github →

chore(CategoryTheory/Products/Basic): cleanup and harmonize (#22325)

Estimated changes

Modified Mathlib/CategoryTheory/Products/Basic.lean

deleted theorem CategoryTheory.Functor.diag_map

deleted theorem CategoryTheory.Functor.diag_obj

modified def CategoryTheory.NatTrans.prod'

deleted theorem CategoryTheory.NatTrans.prod'_app_fst

deleted theorem CategoryTheory.NatTrans.prod'_app_snd