Documentation Verification Report

Fin2

📁 Source: Mathlib/Data/Fin/Fin2.lean

Statistics

Metric	Count
Definitions `Fin2`, `IsLT`, `add`, `cases'`, `castSucc`, `elim0`, `equivFin`, `insertPerm`, `instFintype`, `instInhabitedOfNatNat`, `last`, `left`, `ofFin`, `ofNat'`, `optOfNat`, `remapLeft`, `rev`, `toFin`, `toNat`	19
Theorems `h`, `succ`, `zero`, `equivFin_apply`, `equivFin_symm_apply`, `ofFin_succ`, `ofFin_toFin`, `ofFin_zero`, `rev_castSucc`, `rev_involutive`, `rev_last`, `rev_rev`, `toFin_fs`, `toFin_fz`, `toFin_ofFin`	15
Total	34

Fin2

Definitions

Name	Category	Theorems
`IsLT` 📖	CompData	2 math math: `IsLT.zero`, `IsLT.succ`
`add` 📖	CompOp	2 math math: `Vector3.append_insert`, `Vector3.append_add`
`cases'` 📖	CompOp	—
`castSucc` 📖	CompOp	1 math math: `rev_castSucc`
`elim0` 📖	CompOp	3 math math: `TypeVec.casesNil_append1`, `TypeVec.nilFun_comp`, `TypeVec.typevecCasesNil₂_appendFun`
`equivFin` 📖	CompOp	2 math math: `equivFin_apply`, `equivFin_symm_apply`
`insertPerm` 📖	CompOp	—
`instFintype` 📖	CompOp	—
`instInhabitedOfNatNat` 📖	CompOp	—
`last` 📖	CompOp	1 math math: `rev_last`
`left` 📖	CompOp	1 math math: `Vector3.append_left`
`ofFin` 📖	CompOp	5 math math: `ofFin_zero`, `ofFin_toFin`, `toFin_ofFin`, `ofFin_succ`, `equivFin_symm_apply`
`ofNat'` 📖	CompOp	3 math math: `Dioph.xn_dioph`, `Dioph.pell_dioph`, `Dioph.proj_dioph_of_nat`
`optOfNat` 📖	CompOp	—
`remapLeft` 📖	CompOp	—
`rev` 📖	CompOp	4 math math: `rev_castSucc`, `rev_involutive`, `rev_rev`, `rev_last`
`toFin` 📖	CompOp	5 math math: `toFin_fs`, `ofFin_toFin`, `toFin_ofFin`, `toFin_fz`, `equivFin_apply`
`toNat` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivFin_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Fin2` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivFin` `toFin`	—	—
`equivFin_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Fin2` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivFin` `ofFin`	—	—
`ofFin_succ` 📖	mathematical	—	`ofFin` `fs`	—	—
`ofFin_toFin` 📖	mathematical	—	`ofFin` `toFin`	—	—
`ofFin_zero` 📖	mathematical	—	`ofFin` `fz`	—	—
`rev_castSucc` 📖	mathematical	—	`rev` `castSucc` `fs`	—	—
`rev_involutive` 📖	mathematical	—	`Function.Involutive` `Fin2` `rev`	—	`rev_rev`
`rev_last` 📖	mathematical	—	`rev` `last` `fz`	—	—
`rev_rev` 📖	mathematical	—	`rev`	—	`rev_last` `rev_castSucc`
`toFin_fs` 📖	mathematical	—	`toFin` `fs`	—	—
`toFin_fz` 📖	mathematical	—	`toFin` `fz`	—	—
`toFin_ofFin` 📖	mathematical	—	`toFin` `ofFin`	—	—

Fin2.IsLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`h` 📖	—	—	—	—	—
`succ` 📖	mathematical	—	`Fin2.IsLT`	—	`h`
`zero` 📖	mathematical	—	`Fin2.IsLT`	—	—

(root)

Definitions

Name	Category	Theorems
`Fin2` 📖	CompData	9 math math: `Vector3.append_insert`, `Dioph.diophFn_vec`, `Dioph.xn_dioph`, `Dioph.diophPFun_vec`, `Fin2.rev_involutive`, `Dioph.pell_dioph`, `Fin2.equivFin_apply`, `Dioph.proj_dioph_of_nat`, `Fin2.equivFin_symm_apply`

---

← Back to Index