Documentation Verification Report

Quotient

📁 Source: Mathlib/Data/Fintype/Quotient.lean

Statistics

Metric	Count
Definitions `finChoice`, `finChoiceEquiv`, `finHRecOn`, `finLiftOn`, `finRecOn`, `listChoice`, `finChoice`, `finChoiceEquiv`, `finLiftOn`, `finRecOn`	10
Theorems `eval_finChoice`, `finChoiceEquiv_apply`, `finChoiceEquiv_symm_apply`, `finChoice_eq`, `finHRecOn_mk`, `finLiftOn_empty`, `finLiftOn_mk`, `finRecOn_mk`, `ind_fintype_pi`, `induction_on_fintype_pi`, `listChoice_mk`, `list_ind`, `finChoiceEquiv_apply`, `finChoiceEquiv_symm_apply`, `finChoice_eq`, `finLiftOn_empty`, `finLiftOn_mk`, `finRecOn_mk`	18
Total	28

Quotient

Definitions

Name	Category	Theorems
`finChoice` 📖	CompOp	3 math math: `eval_finChoice`, `finChoiceEquiv_apply`, `finChoice_eq`
`finChoiceEquiv` 📖	CompOp	2 math math: `finChoiceEquiv_apply`, `finChoiceEquiv_symm_apply`
`finHRecOn` 📖	CompOp	1 math math: `finHRecOn_mk`
`finLiftOn` 📖	CompOp	2 math math: `finLiftOn_empty`, `finLiftOn_mk`
`finRecOn` 📖	CompOp	1 math math: `finRecOn_mk`
`listChoice` 📖	CompOp	1 math math: `listChoice_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval_finChoice` 📖	mathematical	—	`eval` `finChoice`	—	`induction_on_fintype_pi` `finChoice_eq`
`finChoiceEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `piSetoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `finChoiceEquiv` `finChoice`	—	—
`finChoiceEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `piSetoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finChoiceEquiv` `eval`	—	—
`finChoice_eq` 📖	mathematical	—	`finChoice` `piSetoid`	—	`Finset.mem_univ` `liftOn.congr_simp` `map.congr_simp`
`finHRecOn_mk` 📖	mathematical	—	`finHRecOn`	—	`eval_finChoice` `finChoice_eq`
`finLiftOn_empty` 📖	mathematical	—	`finLiftOn` `IsEmpty.elim`	—	—
`finLiftOn_mk` 📖	mathematical	—	`finLiftOn`	—	`finChoice_eq`
`finRecOn_mk` 📖	mathematical	—	`finRecOn`	—	—
`ind_fintype_pi` 📖	—	—	—	—	`list_ind` `Finset.mem_univ`
`induction_on_fintype_pi` 📖	—	—	—	—	`ind_fintype_pi`
`listChoice_mk` 📖	mathematical	—	`listChoice` `piSetoid`	—	`listChoice.eq_def` `List.Pi.cons_eta`
`list_ind` 📖	—	—	—	—	`List.Pi.cons_eta` `List.Pi.cons_map`

Trunc

Definitions

Name	Category	Theorems
`finChoice` 📖	CompOp	3 math math: `MultilinearMap.dfinsuppFamily_apply_support'`, `finChoice_eq`, `finChoiceEquiv_apply`
`finChoiceEquiv` 📖	CompOp	2 math math: `finChoiceEquiv_symm_apply`, `finChoiceEquiv_apply`
`finLiftOn` 📖	CompOp	2 math math: `finLiftOn_mk`, `finLiftOn_empty`
`finRecOn` 📖	CompOp	1 math math: `finRecOn_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finChoiceEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Trunc` `EquivLike.toFunLike` `Equiv.instEquivLike` `finChoiceEquiv` `finChoice`	—	—
`finChoiceEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Trunc` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finChoiceEquiv` `map`	—	—
`finChoice_eq` 📖	mathematical	—	`finChoice`	—	`instSubsingletonTrunc`
`finLiftOn_empty` 📖	mathematical	—	`finLiftOn` `IsEmpty.elim`	—	`Quotient.finLiftOn_empty`
`finLiftOn_mk` 📖	mathematical	—	`finLiftOn` `trueSetoid`	—	—
`finRecOn_mk` 📖	mathematical	—	`finRecOn` `trueSetoid`	—	`eq`

---

← Back to Index