Mathlib Changelog
v3
Changelog
About
Github
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
src/data/vector3.lean
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