Def CategoryTheory.sum.associativity

Modification history

2024-08-19 18:48
Mathlib/CategoryTheory/Sums/Associator.lean
chore: remove unnecessary uses of CategoryTheory.Equivalence.mk (#15919) …
Modified CategoryTheory.sum.associativityView on Github →
2024-07-20 07:03
Mathlib/CategoryTheory/Sums/Associator.lean
chore(*): use ⊕ notation for `Sum` (#14934)
Modified CategoryTheory.sum.associativityView on Github →
2023-02-28 18:30
Mathlib/CategoryTheory/Sums/Associator.lean
feat: Port CategoryTheory.Sums.Associator (#2447)
Added CategoryTheory.sum.associativityView on Github →