Theorems · Theorem · dynamical systems
Function.iterate_add_apply
∀ {α : Type u} (f : α → α) (m n : ℕ) (x : α), f^[m + n] x = f^[m] (f^[n] x)- Defined in
- Mathlib.Logic.Function.Iterate
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 11 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_addproof · cited by 11
Cited by25
Results whose statement or proof uses this declaration.
- PerfectClosure.mk_eq_iffproof · cited by 3
- Dynamics.IsDynCoverOf.iterate_le_powproof · cited by 2
- Function.periodic_iterate_iffproof · cited by 2
- WittVector.iterate_verschiebung_mulproof · cited by 2
- Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterateproof · cited by 2
- iter_deriv_inv_linearproof · cited by 2
- Function.IsPeriodicPt.iterate_mod_applyproof · cited by 2
- Function.periodicOrbit_apply_iterate_eqproof · cited by 1
- Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_Tproof · cited by 1
- Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_Uproof · cited by 1
- Function.periodicPts_subset_rangeproof · cited by 1
- LieSubmodule.ucs_addproof · cited by 1