Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-18 19:43 ab7d39b0

View on Github →

feat(data/vector2): update_nth (#1334)

feat(data/vector2): update_nth
naming and docstrings
remove double namespace fom vector.nth_mem

Estimated changes

Modified src/data/fin.lean

added theorem fin.exists_iff

modified theorem fin.find_eq_some_iff

added theorem fin.forall_iff

modified theorem fin.mem_find_iff

Modified src/data/list/basic.lean

added theorem list.nth_le_update_nth_eq

added theorem list.nth_le_update_nth_of_ne

Modified src/data/vector2.lean

added theorem vector.mem_iff_nth

added theorem vector.nodup_iff_nth_inj

added theorem vector.nth_mem

added theorem vector.nth_update_nth_eq_if

added theorem vector.nth_update_nth_of_ne

added theorem vector.nth_update_nth_same

added def vector.update_nth