Commit 2023-01-17 17:59 8cc7ae9e

View on Github →

feat: port Data.List.ofFn (#1630)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/OfFn.lean

added def List.equivSigmaTuple

added theorem List.exists_iff_exists_tuple

added theorem List.forall_iff_forall_tuple

added theorem List.forall_mem_ofFn_iff

added theorem List.get?_ofFn

added theorem List.get_ofFn

added theorem List.last_ofFn

added theorem List.last_ofFn_succ

added theorem List.length_ofFn

added theorem List.map_ofFn

added theorem List.mem_ofFn

added theorem List.nthLe_ofFn'

added theorem List.nthLe_ofFn

added def List.ofFnRec

added theorem List.ofFnRec_ofFn

added theorem List.ofFn_add

added theorem List.ofFn_congr

added theorem List.ofFn_const

added theorem List.ofFn_eq_nil_iff

added theorem List.ofFn_get

added theorem List.ofFn_inj'

added theorem List.ofFn_inj

added theorem List.ofFn_injective

added theorem List.ofFn_mul'

added theorem List.ofFn_mul

added theorem List.ofFn_nthLe

added theorem List.ofFn_succ'

added theorem List.ofFn_succ

added theorem List.ofFn_zero