Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 14:26 34993236

View on Github →

chore(data/vector3): Make linter happy (#10998) and clean up a bit.

Estimated changes

modified theorem exists_vector_succ
modified theorem exists_vector_zero
modified def vector3.append
modified theorem vector3.append_add
modified theorem vector3.append_cons
modified theorem vector3.append_insert
modified theorem vector3.append_left
modified theorem vector3.append_nil
modified def vector3.cons
modified def vector3.cons_elim
modified theorem vector3.cons_elim_cons
modified theorem vector3.cons_fs
modified theorem vector3.cons_fz
modified theorem vector3.cons_head_tail
modified theorem vector3.eq_nil
modified def vector3.head
modified def vector3.insert
modified theorem vector3.insert_fs
modified theorem vector3.insert_fz
modified def vector3.nil
modified def vector3.nil_elim
modified def vector3.nth
modified def vector3.of_fn
modified theorem vector3.rec_on_cons
modified theorem vector3.rec_on_nil
modified def vector3.tail
modified def vector_all
modified theorem vector_all_iff_forall
modified theorem vector_allp.imp
modified def vector_allp
modified theorem vector_allp_cons
modified theorem vector_allp_iff_forall
modified theorem vector_allp_nil
modified theorem vector_allp_singleton
modified def vector_ex
modified theorem vector_ex_iff_exists