Documentation Verification Report

Vector3

📁 Source: Mathlib/Data/Vector3.lean

Statistics

Metric	Count
Definitions `Vector3`, `append`, `cons`, `consElim`, `head`, `insert`, `nil`, `nilElim`, `nth`, `ofFn`, `recOn`, `tail`, `unexpandCons`, `unexpandNil`, `«term_::_»`, `VectorAll`, `VectorAllP`, `VectorEx`, `instInhabitedVector3`	19
Theorems `append_add`, `append_cons`, `append_insert`, `append_left`, `append_nil`, `consElim_cons`, `cons_fs`, `cons_fz`, `cons_head_tail`, `eq_nil`, `insert_fs`, `insert_fz`, `recOn_cons`, `recOn_nil`, `imp`, `exists_vector_succ`, `exists_vector_zero`, `vectorAllP_cons`, `vectorAllP_iff_forall`, `vectorAllP_nil`, `vectorAllP_singleton`, `vectorAll_iff_forall`, `vectorEx_iff_exists`	23
Total	42

Vector3

Definitions

Name	Category	Theorems
`append` 📖	CompOp	5 math math: `append_insert`, `append_nil`, `append_add`, `append_left`, `append_cons`
`cons` 📖	CompOp	13 math math: `Dioph.vec_ex1_dioph`, `vectorAllP_singleton`, `cons_fs`, `exists_vector_succ`, `cons_head_tail`, `cons_fz`, `insert_fz`, `consElim_cons`, `insert_fs`, `Dioph.diophFn_vec_comp1`, `recOn_cons`, `vectorAllP_cons`, `append_cons`
`consElim` 📖	CompOp	1 math math: `consElim_cons`
`head` 📖	CompOp	1 math math: `cons_head_tail`
`insert` 📖	CompOp	3 math math: `append_insert`, `insert_fz`, `insert_fs`
`nil` 📖	CompOp	6 math math: `append_nil`, `eq_nil`, `vectorAllP_nil`, `vectorAllP_singleton`, `exists_vector_zero`, `recOn_nil`
`nilElim` 📖	CompOp	—
`nth` 📖	CompOp	—
`ofFn` 📖	CompOp	—
`recOn` 📖	CompOp	—
`tail` 📖	CompOp	1 math math: `cons_head_tail`
`unexpandCons` 📖	CompOp	—
`unexpandNil` 📖	CompOp	—
`«term_::_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_add` 📖	mathematical	—	`append` `Fin2.add`	—	—
`append_cons` 📖	mathematical	—	`append` `cons`	—	—
`append_insert` 📖	mathematical	—	`insert` `append` `Fin2` `Fin2.add` `Vector3`	—	`insert_fs`
`append_left` 📖	mathematical	—	`append` `Fin2.left`	—	—
`append_nil` 📖	mathematical	—	`append` `nil`	—	—
`consElim_cons` 📖	mathematical	—	`consElim` `cons`	—	—
`cons_fs` 📖	mathematical	—	`cons` `Fin2.fs`	—	—
`cons_fz` 📖	mathematical	—	`cons` `Fin2.fz`	—	—
`cons_head_tail` 📖	mathematical	—	`cons` `head` `tail`	—	—
`eq_nil` 📖	mathematical	—	`nil`	—	—
`insert_fs` 📖	mathematical	—	`insert` `cons` `Fin2.fs`	—	—
`insert_fz` 📖	mathematical	—	`insert` `Fin2.fz` `cons`	—	—
`recOn_cons` 📖	mathematical	—	`cons`	—	—
`recOn_nil` 📖	mathematical	—	`nil`	—	—

VectorAllP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`imp` 📖	—	`VectorAllP`	—	—	`vectorAllP_iff_forall`

(root)

Definitions

Name	Category	Theorems
`Vector3` 📖	CompOp	5 math math: `Vector3.append_insert`, `Dioph.vec_ex1_dioph`, `Dioph.diophPFun_vec`, `Dioph.diophFn_vec_comp1`, `Dioph.dioph_comp`
`VectorAll` 📖	MathDef	1 math math: `vectorAll_iff_forall`
`VectorAllP` 📖	MathDef	4 math math: `vectorAllP_nil`, `vectorAllP_singleton`, `vectorAllP_iff_forall`, `vectorAllP_cons`
`VectorEx` 📖	MathDef	1 math math: `vectorEx_iff_exists`
`instInhabitedVector3` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_vector_succ` 📖	mathematical	—	`Vector3.cons`	—	`Vector3.cons_head_tail`
`exists_vector_zero` 📖	mathematical	—	`Vector3.nil`	—	`Vector3.eq_nil`
`vectorAllP_cons` 📖	mathematical	—	`VectorAllP` `Vector3.cons`	—	—
`vectorAllP_iff_forall` 📖	mathematical	—	`VectorAllP`	—	—
`vectorAllP_nil` 📖	mathematical	—	`VectorAllP` `Vector3.nil`	—	—
`vectorAllP_singleton` 📖	mathematical	—	`VectorAllP` `Vector3.cons` `Vector3.nil`	—	—
`vectorAll_iff_forall` 📖	mathematical	—	`VectorAll`	—	—
`vectorEx_iff_exists` 📖	mathematical	—	`VectorEx`	—	`exists_vector_zero` `exists_vector_succ`

---

← Back to Index