Theorems · Theorem · dynamical systems
Function.iterate_add
∀ {α : Type u} (f : α → α) (m n : ℕ), f^[m + n] = f^[m] ∘ f^[n]- Defined in
- Mathlib.Logic.Function.Iterate
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.iteratestatement · cited by 740
Cited by11
Results whose statement or proof uses this declaration.
- Function.iterate_add_applyproof · cited by 24
- le_total_of_directedproof · cited by 2
- Function.IsPeriodicPt.left_of_addproof · cited by 2
- Function.Involutive.iterate_oddproof · cited by 2
- MeasureTheory.AEEqFun.compQuasiMeasurePreserving_iterateproof · cited by 1
- le_total_of_codirectedproof · cited by 1
- JacobsonNoether.exist_pow_eq_zero_of_leproof · cited by 1
- MeasureTheory.Conservative.frequently_measure_inter_ne_zeroproof · cited by 1
- PerfectClosure.eq_iffproof · cited by 0
- MeasureTheory.Lp.compMeasurePreserving_iterateproof · cited by 0
- Function.IsPeriodicPt.addproof · cited by 0