Theorems · Theorem · dynamical systems
Function.iterate_id
∀ {α : Type u} (n : ℕ), id^[n] = id- Defined in
- Mathlib.Logic.Function.Iterate
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.iteratestatement and proof · cited by 740
- Function.iterate_succproof · cited by 19
Cited by8
Results whose statement or proof uses this declaration.
- Function.id_le_iterate_of_id_leproof · cited by 4
- Function.iterate_le_id_of_le_idproof · cited by 3
- Function.Involutive.iterate_two_mulproof · cited by 3
- MonoidHom.map_iterate_frobeniusEquiv_symmproof · cited by 1
- CircleDeg1Lift.translationNumber_oneproof · cited by 1
- WittVector.mem_span_p_pow_iff_le_coeff_eq_zeroproof · cited by 1
- MeasureTheory.Conservative.idproof · cited by 1
- Ordinal.nfp_idproof · cited by 0