Theorem CategoryTheory.forget₂_comp_apply

Modification history

2025-01-17 14:00

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809) …

Modified CategoryTheory.forget₂_comp_apply View on Github →

2023-12-27 10:11

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

feat(Algebra/Homology): computation of the connecting homomorphism of the homology sequence (#8771) …

Added CategoryTheory.forget₂_comp_apply View on Github →