Documentation Verification Report

Reflection

📁 Source: Mathlib/Data/Fin/Tuple/Reflection.lean

Statistics

Metric	Count
Definitions `prod_univ_ofNat`, `sum_univ_ofNat`, `Exists`, `Forall`, `etaExpand`, `map`, `mkProdEqQ`, `mkSumEqQ`, `prod`, `seq`, `sum`	11
Theorems `etaExpand_eq`, `exists_iff`, `forall_iff`, `map_eq`, `prod_eq`, `seq_eq`, `sum_eq`	7
Total	18

Fin

Definitions

Name	Category	Theorems
`prod_univ_ofNat` 📖	CompOp	—
`sum_univ_ofNat` 📖	CompOp	—

FinVec

Definitions

Name	Category	Theorems
`Exists` 📖	MathDef	1 math math: `exists_iff`
`Forall` 📖	MathDef	1 math math: `forall_iff`
`etaExpand` 📖	CompOp	1 math math: `etaExpand_eq`
`map` 📖	CompOp	1 math math: `map_eq`
`mkProdEqQ` 📖	CompOp	—
`mkSumEqQ` 📖	CompOp	—
`prod` 📖	CompOp	1 math math: `prod_eq`
`seq` 📖	CompOp	1 math math: `seq_eq`
`sum` 📖	CompOp	1 math math: `sum_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`etaExpand_eq` 📖	mathematical	—	`etaExpand`	—	`map_eq`
`exists_iff` 📖	mathematical	—	`Exists`	—	—
`forall_iff` 📖	mathematical	—	`Forall`	—	—
`map_eq` 📖	mathematical	—	`map`	—	`seq_eq`
`prod_eq` 📖	mathematical	—	`prod` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toOne` `Finset.prod` `Finset.univ` `Fin.fintype`	—	`Fintype.prod_unique` `Fin.prod_univ_castSucc` `prod.eq_3`
`seq_eq` 📖	mathematical	—	`seq`	—	`Unique.instSubsingleton` `Fin.isEmpty'` `Matrix.cons_val_succ`
`sum_eq` 📖	mathematical	—	`sum` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toZero` `Finset.sum` `Finset.univ` `Fin.fintype`	—	`Fintype.sum_unique` `Fin.sum_univ_castSucc` `sum.eq_3`

---

← Back to Index