Iterate

Statistics

Metric	Count
Definitions	0
Theorems `getElem?_iterate`, `getElem_iterate`, `iterate_add`, `iterate_eq_nil`, `length_iterate`, `mem_iterate`, `range_map_iterate`, `take_iterate`	8
Total	8

Name	Kind	Assumes	Proves	Validates	Depends On
`getElem?_iterate` 📖	mathematical	—	`iterate` `Nat.iterate`	—	`length_iterate` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Nat.instCanonicallyOrderedAdd`
`getElem_iterate` 📖	mathematical	`iterate`	`iterate` `Nat.iterate`	—	`getElem?_iterate` `length_iterate`
`iterate_add` 📖	mathematical	—	`iterate` `Nat.iterate`	—	`zero_add` `iterate.eq_2` `add_right_comm` `Nat.iterate.eq_2`
`iterate_eq_nil` 📖	mathematical	—	`iterate`	—	`length_iterate`
`length_iterate` 📖	mathematical	—	`iterate`	—	—
`mem_iterate` 📖	mathematical	—	`iterate` `Nat.iterate`	—	`getElem_iterate` `length_iterate`
`range_map_iterate` 📖	mathematical	—	`Nat.iterate` `iterate`	—	`length_iterate` `getElem_iterate`
`take_iterate` 📖	mathematical	—	`iterate`	—	`range_map_iterate`

---