Def CategoryTheory.NatTrans.ofSequence

Modification history

2024-05-30 18:01
Mathlib/CategoryTheory/Functor/OfSequence.lean
feat(CategoryTheory): constructor for functors from the category `ℕ` (#13223) …
Added CategoryTheory.NatTrans.ofSequenceView on Github →