Commit 2021-08-15 21:24 fc7da8d9

View on Github →

chore(data/vector3): extract to a new file (#8669) This is simply a file move, with no other changes other than a minimal docstring. In it's old location this was very hard to find.

Estimated changes

Created src/data/vector3.lean

added theorem exists_vector_succ

added theorem exists_vector_zero

added def vector3.append

added theorem vector3.append_add

added theorem vector3.append_cons

added theorem vector3.append_insert

added theorem vector3.append_left

added theorem vector3.append_nil

added def vector3.cons

added def vector3.cons_elim

added theorem vector3.cons_elim_cons

added theorem vector3.cons_fs

added theorem vector3.cons_fz

added theorem vector3.cons_head_tail

added theorem vector3.eq_nil

added def vector3.head

added def vector3.insert

added theorem vector3.insert_fs

added theorem vector3.insert_fz

added def vector3.nil

added def vector3.nil_elim

added def vector3.nth

added def vector3.of_fn

added theorem vector3.rec_on_cons

added theorem vector3.rec_on_nil

added def vector3.tail

added def vector3

added def vector_all

added theorem vector_all_iff_forall

added theorem vector_allp.imp

added def vector_allp

added theorem vector_allp_cons

added theorem vector_allp_iff_forall

added theorem vector_allp_nil

added theorem vector_allp_singleton

added def vector_ex

added theorem vector_ex_iff_exists

Modified src/number_theory/dioph.lean

deleted theorem exists_vector_succ

deleted theorem exists_vector_zero

deleted def vector3.append

deleted theorem vector3.append_add

deleted theorem vector3.append_cons

deleted theorem vector3.append_insert

deleted theorem vector3.append_left

deleted theorem vector3.append_nil

deleted def vector3.cons

deleted def vector3.cons_elim

deleted theorem vector3.cons_elim_cons

deleted theorem vector3.cons_fs

deleted theorem vector3.cons_fz

deleted theorem vector3.cons_head_tail

deleted theorem vector3.eq_nil

deleted def vector3.head

deleted def vector3.insert

deleted theorem vector3.insert_fs

deleted theorem vector3.insert_fz

deleted def vector3.nil

deleted def vector3.nil_elim

deleted def vector3.nth

deleted def vector3.of_fn

deleted theorem vector3.rec_on_cons

deleted theorem vector3.rec_on_nil

deleted def vector3.tail

deleted def vector3

deleted def vector_all

deleted theorem vector_all_iff_forall

deleted theorem vector_allp.imp

deleted def vector_allp

deleted theorem vector_allp_cons

deleted theorem vector_allp_iff_forall

deleted theorem vector_allp_nil

deleted theorem vector_allp_singleton

deleted def vector_ex

deleted theorem vector_ex_iff_exists