Theorem CategoryTheory.Functor.OfSequence.map_id

Modification history

2025-09-24 05:32

Mathlib/CategoryTheory/Functor/OfSequence.lean

chore: replace omega with cutsat where possible (#29461) …

Modified CategoryTheory.Functor.OfSequence.map_id View on Github →

2024-05-30 18:01

Mathlib/CategoryTheory/Functor/OfSequence.lean

feat(CategoryTheory): constructor for functors from the category `ℕ` (#13223) …

Added CategoryTheory.Functor.OfSequence.map_id View on Github →