Commit 2023-06-09 04:21 419351fa

View on Github →

feat: port Data.Vector3 (#1204)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Vector3.lean

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.consElim

added theorem Vector3.consElim_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.nilElim

added def Vector3.nth

added def Vector3.ofFn

added theorem Vector3.recOn_cons

added theorem Vector3.recOn_nil

added def Vector3.tail

added def Vector3.unexpandCons

added def Vector3.unexpandNil

added def Vector3

added def VectorAll

added theorem VectorAllP.imp

added def VectorAllP

added def VectorEx

added theorem exists_vector_succ

added theorem exists_vector_zero

added theorem vectorAllP_cons

added theorem vectorAllP_iff_forall

added theorem vectorAllP_nil

added theorem vectorAllP_singleton

added theorem vectorAll_iff_forall

added theorem vectorEx_iff_exists