Documentation Verification Report

FromTypes

📁 Source: Mathlib/Logic/Function/FromTypes.lean

Statistics

Metric	Count
Definitions `FromTypes`, `const`, `inhabited`, `fromTypes_cons_equiv`, `fromTypes_nil_equiv`, `fromTypes_succ_equiv`, `fromTypes_zero_equiv`	7
Theorems `const_succ`, `const_succ_apply`, `const_zero`, `fromTypes_cons`, `fromTypes_cons_equiv_apply`, `fromTypes_cons_equiv_symm_apply`, `fromTypes_nil`, `fromTypes_nil_equiv_apply`, `fromTypes_nil_equiv_symm_apply`, `fromTypes_succ`, `fromTypes_succ_equiv_apply`, `fromTypes_succ_equiv_symm_apply`, `fromTypes_zero`, `fromTypes_zero_equiv_apply`, `fromTypes_zero_equiv_symm_apply`	15
Total	22

Function

Definitions

Name	Category	Theorems
`FromTypes` 📖	CompOp	17 math math: `fromTypes_cons_equiv_symm_apply`, `FromTypes.fromTypes_fin_const`, `fromTypes_nil_equiv_apply`, `fromTypes_zero_equiv_symm_apply`, `fromTypes_cons`, `fromTypes_succ_equiv_symm_apply`, `FromTypes.curryEquiv_symm_apply`, `fromTypes_zero`, `FromTypes.uncurry_two_eq_uncurry`, `fromTypes_nil`, `fromTypes_succ_equiv_apply`, `OfArity.uncurry_two_eq_uncurry`, `fromTypes_zero_equiv_apply`, `fromTypes_cons_equiv_apply`, `fromTypes_succ`, `FromTypes.curryEquiv_apply`, `fromTypes_nil_equiv_symm_apply`
`fromTypes_cons_equiv` 📖	CompOp	2 math math: `fromTypes_cons_equiv_symm_apply`, `fromTypes_cons_equiv_apply`
`fromTypes_nil_equiv` 📖	CompOp	2 math math: `fromTypes_nil_equiv_apply`, `fromTypes_nil_equiv_symm_apply`
`fromTypes_succ_equiv` 📖	CompOp	2 math math: `fromTypes_succ_equiv_symm_apply`, `fromTypes_succ_equiv_apply`
`fromTypes_zero_equiv` 📖	CompOp	2 math math: `fromTypes_zero_equiv_symm_apply`, `fromTypes_zero_equiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromTypes_cons` 📖	mathematical	—	`FromTypes` `Matrix.vecCons`	—	`fromTypes_succ`
`fromTypes_cons_equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `FromTypes` `Matrix.vecCons` `EquivLike.toFunLike` `Equiv.instEquivLike` `fromTypes_cons_equiv`	—	—
`fromTypes_cons_equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `FromTypes` `Matrix.vecCons` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `fromTypes_cons_equiv`	—	—
`fromTypes_nil` 📖	mathematical	—	`FromTypes` `Matrix.vecEmpty`	—	`fromTypes_zero`
`fromTypes_nil_equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `FromTypes` `Matrix.vecEmpty` `EquivLike.toFunLike` `Equiv.instEquivLike` `fromTypes_nil_equiv`	—	—
`fromTypes_nil_equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `FromTypes` `Matrix.vecEmpty` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `fromTypes_nil_equiv`	—	—
`fromTypes_succ` 📖	mathematical	—	`FromTypes`	—	—
`fromTypes_succ_equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `FromTypes` `EquivLike.toFunLike` `Equiv.instEquivLike` `fromTypes_succ_equiv`	—	—
`fromTypes_succ_equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `FromTypes` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `fromTypes_succ_equiv`	—	—
`fromTypes_zero` 📖	mathematical	—	`FromTypes`	—	—
`fromTypes_zero_equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `FromTypes` `EquivLike.toFunLike` `Equiv.instEquivLike` `fromTypes_zero_equiv`	—	—
`fromTypes_zero_equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `FromTypes` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `fromTypes_zero_equiv`	—	—

Function.FromTypes

Definitions

Name	Category	Theorems
`const` 📖	CompOp	3 math math: `const_succ_apply`, `const_succ`, `const_zero`
`inhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_succ` 📖	mathematical	—	`const` `Matrix.vecTail`	—	—
`const_succ_apply` 📖	mathematical	—	`const` `Matrix.vecTail`	—	—
`const_zero` 📖	mathematical	—	`const`	—	—

---

← Back to Index