Documentation Verification Report

Reflection

📁 Source: Mathlib/Data/Matrix/Reflection.lean

Statistics

Metric	Count
Definitions `Exists`, `Forall`, `dotProductᵣ`, `etaExpand`, `mulVecᵣ`, `mulᵣ`, `transposeᵣ`, `vecMulᵣ`	8
Theorems `dotProductᵣ_eq`, `etaExpand_eq`, `exists_iff`, `forall_iff`, `mulVecᵣ_eq`, `mulᵣ_eq`, `transposeᵣ_eq`, `vecMulᵣ_eq`	8
Total	16

Matrix

Definitions

Name	Category	Theorems
`Exists` 📖	MathDef	1 math math: `exists_iff`
`Forall` 📖	MathDef	1 math math: `forall_iff`
`dotProductᵣ` 📖	CompOp	1 math math: `dotProductᵣ_eq`
`etaExpand` 📖	CompOp	1 math math: `etaExpand_eq`
`mulVecᵣ` 📖	CompOp	1 math math: `mulVecᵣ_eq`
`mulᵣ` 📖	CompOp	1 math math: `mulᵣ_eq`
`transposeᵣ` 📖	CompOp	1 math math: `transposeᵣ_eq`
`vecMulᵣ` 📖	CompOp	1 math math: `vecMulᵣ_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dotProductᵣ_eq` 📖	mathematical	—	`dotProductᵣ` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `dotProduct` `Fin.fintype`	—	`FinVec.sum_eq` `Finset.sum_congr` `FinVec.seq_eq` `FinVec.map_eq`
`etaExpand_eq` 📖	mathematical	—	`etaExpand`	—	`FinVec.etaExpand_eq`
`exists_iff` 📖	mathematical	—	`Exists`	—	`Fin.exists_fin_zero_pi` `Fin.exists_fin_succ_pi`
`forall_iff` 📖	mathematical	—	`Forall`	—	`Fin.forall_fin_zero_pi` `Fin.forall_fin_succ_pi`
`mulVecᵣ_eq` 📖	mathematical	—	`mulVecᵣ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `mulVec` `Fin.fintype`	—	`dotProductᵣ_eq` `FinVec.map_eq`
`mulᵣ_eq` 📖	mathematical	—	`mulᵣ` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Fin.fintype`	—	`dotProductᵣ_eq` `FinVec.map_eq`
`transposeᵣ_eq` 📖	mathematical	—	`transposeᵣ` `transpose`	—	`subsingleton_of_empty_left` `Fin.isEmpty'` `ext` `FinVec.map_eq` `cons_val_succ`
`vecMulᵣ_eq` 📖	mathematical	—	`vecMulᵣ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `vecMul` `Fin.fintype`	—	`dotProductᵣ_eq` `FinVec.map_eq`

---

← Back to Index