Theorem CategoryTheory.Functor.OfSequence.map_le_succ

Modification history

2025-12-04 09:22
Mathlib/CategoryTheory/Functor/OfSequence.lean
feat(Tactic): add `lia` as an alias for `cutsat` and use it throughout (#32376) …
Modified CategoryTheory.Functor.OfSequence.map_le_succView on Github →
2025-09-24 05:32
Mathlib/CategoryTheory/Functor/OfSequence.lean
chore: replace omega with cutsat where possible (#29461) …
Modified CategoryTheory.Functor.OfSequence.map_le_succView 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_le_succView on Github →