Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-09 19:44 0dde2cb8

View on Github →

feat(data/list/chain): Lemma for chain r a (list.range n.succ) (#12990)

Estimated changes

Modified src/data/list/chain.lean

added theorem list.chain'_append_cons_cons

Modified src/data/list/range.lean

added theorem list.chain'_range_succ

added theorem list.chain_range_succ

Modified src/data/nat/basic.lean

added theorem nat.exists_lt_succ

added theorem nat.forall_lt_succ