ListOfFn

Statistics

Metric	Count
Definitions	0
Theorems `mem_list_prod`, `mem_list_sum`, `mem_nsmul`, `mem_pow`, `mem_prod_list_ofFn`, `mem_sum_list_ofFn`	6
Total	6

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_list_prod` 📖	mathematical	—	`Set` `instMembership` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `one` `MulOne.toOne` `Elem`	—	`List.map_ofFn`
`mem_list_sum` 📖	mathematical	—	`Set` `instMembership` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `zero` `AddZero.toZero` `Elem`	—	`mem_sum_list_ofFn` `List.exists_iff_exists_tuple` `List.map_ofFn` `List.ofFn_inj'`
`mem_nsmul` 📖	mathematical	—	`Set` `instMembership` `NSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toAdd`	—	`mem_sum_list_ofFn` `List.ofFn_const` `List.sum_replicate`
`mem_pow` 📖	mathematical	—	`Set` `instMembership` `NPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul`	—	`mem_prod_list_ofFn` `List.ofFn_const` `List.prod_replicate`
`mem_prod_list_ofFn` 📖	mathematical	—	`Set` `instMembership` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `one` `MulOne.toOne`	—	`Fin.cons_zero` `Fin.cons_succ`
`mem_sum_list_ofFn` 📖	mathematical	—	`Set` `instMembership` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `zero` `AddZero.toZero`	—	`Fin.exists_fin_zero_pi` `mem_zero` `Fin.exists_fin_succ_pi` `Fin.cons_zero` `Fin.cons_succ` `mem_add` `exists_exists_eq_and` `SetCoe.exists`

---