Documentation Verification Report

Cast

📁 Source: Mathlib/Combinatorics/Quiver/Cast.lean

Statistics

Metric	Count
Definitions `cast`, `cast`	2
Theorems `cast_cast`, `cast_eq_cast`, `cast_eq_iff_heq`, `cast_heq`, `cast_rfl_rfl`, `eq_cast_iff_heq`, `cast_cast`, `cast_cons`, `cast_eq_cast`, `cast_eq_iff_heq`, `cast_heq`, `cast_nil`, `cast_rfl_rfl`, `eq_cast_iff_heq`, `cast_eq_of_cons_eq_cons`, `eq_nil_of_length_zero`, `hom_cast_eq_of_cons_eq_cons`	17
Total	19

Quiver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_eq_of_cons_eq_cons` 📖	mathematical	`Path.cons`	`Path.cast` `Path.obj_eq_of_cons_eq_cons`	—	`Path.obj_eq_of_cons_eq_cons` `Path.cast_eq_iff_heq` `Path.heq_of_cons_eq_cons`
`eq_nil_of_length_zero` 📖	mathematical	`Path.length`	`Path.cast` `Path.eq_of_length_zero` `Path.nil`	—	`Path.eq_of_length_zero`
`hom_cast_eq_of_cons_eq_cons` 📖	mathematical	`Path.cons`	`Hom.cast` `Path.obj_eq_of_cons_eq_cons`	—	`Path.obj_eq_of_cons_eq_cons` `Hom.cast_eq_iff_heq` `Path.hom_heq_of_cons_eq_cons`

Quiver.Hom

Definitions

Name	Category	Theorems
`cast` 📖	CompOp	8 math math: `cast_cast`, `Quiver.Path.cast_cons`, `Quiver.hom_cast_eq_of_cons_eq_cons`, `cast_eq_cast`, `cast_rfl_rfl`, `cast_heq`, `eq_cast_iff_heq`, `cast_eq_iff_heq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_cast` 📖	mathematical	—	`cast`	—	—
`cast_eq_cast` 📖	mathematical	—	`cast` `Quiver.Hom`	—	—
`cast_eq_iff_heq` 📖	mathematical	—	`cast` `Quiver.Hom`	—	`cast_eq_cast`
`cast_heq` 📖	mathematical	—	`Quiver.Hom` `cast`	—	—
`cast_rfl_rfl` 📖	mathematical	—	`cast`	—	—
`eq_cast_iff_heq` 📖	mathematical	—	`cast` `Quiver.Hom`	—	`cast_eq_iff_heq`

Quiver.Path

Definitions

Name	Category	Theorems
`cast` 📖	CompOp	11 math math: `cast_cast`, `Quiver.eq_nil_of_length_zero`, `cast_eq_cast`, `eq_cast_iff_heq`, `Quiver.cast_eq_of_cons_eq_cons`, `cast_heq`, `cast_cons`, `cast_nil`, `cast_eq_iff_heq`, `Quiver.SingleObj.listToPath_pathToList`, `cast_rfl_rfl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_cast` 📖	mathematical	—	`cast`	—	—
`cast_cons` 📖	mathematical	—	`cast` `cons` `Quiver.Hom.cast`	—	—
`cast_eq_cast` 📖	mathematical	—	`cast` `Quiver.Path`	—	—
`cast_eq_iff_heq` 📖	mathematical	—	`cast` `Quiver.Path`	—	`cast_eq_cast`
`cast_heq` 📖	mathematical	—	`Quiver.Path` `cast`	—	`cast_eq_cast`
`cast_nil` 📖	mathematical	—	`cast` `nil`	—	—
`cast_rfl_rfl` 📖	mathematical	—	`cast`	—	—
`eq_cast_iff_heq` 📖	mathematical	—	`cast` `Quiver.Path`	—	`cast_eq_iff_heq`

---

← Back to Index