Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-17 22:49 bac655d3

View on Github →

feature(data/vector2, data/list): add insert_nth for vectors and lists

Estimated changes

Modified data/equiv/fin.lean

Modified data/fin.lean

added theorem fin.cast_succ_inj

added theorem fin.eq_iff_veq

added theorem fin.pred_inj

Modified data/list/basic.lean

added def list.insert_nth

added theorem list.insert_nth_comm

added theorem list.insert_nth_nil

added theorem list.insert_nth_remove_nth_of_ge

added theorem list.insert_nth_remove_nth_of_le

added theorem list.length_insert_nth

added theorem list.modify_nth_tail_id

added theorem list.modify_nth_tail_modify_nth_tail

added theorem list.modify_nth_tail_modify_nth_tail_le

added theorem list.modify_nth_tail_modify_nth_tail_same

added theorem list.remove_nth_insert_nth

Modified data/vector2.lean

added def vector.insert_nth

added theorem vector.insert_nth_comm

added theorem vector.insert_nth_val

added def vector.m_of_fn

added def vector.mmap

added theorem vector.remove_nth_insert_nth

added theorem vector.remove_nth_insert_nth_ne

added theorem vector.remove_nth_val

deleted def vector.{u}