Theorems · Theorem
List.getElem_iterate
∀ {α : Type u_1} (f : α → α) (a : α) (n i : ℕ) (h : i < (List.iterate f a n).length), (List.iterate f a n)[i] = f^[i] a- Defined in
- Mathlib.Data.List.Iterate
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.iteratestatement · cited by 740
- List.iteratestatement and proof · cited by 15
- List.length_iterateproof · cited by 6
- List.getElem?_iterateproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- Equiv.Perm.getElem_toListproof · cited by 3
- Equiv.Perm.toList_formPerm_nontrivialproof · cited by 1
- List.range_map_iterateproof · cited by 1
- List.mem_iterateproof · cited by 0
- Equiv.Perm.toList_getElem_zeroproof · cited by 0