Theorems · Theorem · dynamical systems
Function.iterate_zero_apply
∀ {α : Type u} (f : α → α) (x : α), f^[0] x = x- Defined in
- Mathlib.Logic.Function.Iterate
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 7 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 by16
Results whose statement or proof uses this declaration.
- Function.periodicOrbit_chainproof · cited by 1
- Polynomial.iterate_derivative_X_pow_eq_natCast_mulproof · cited by 1
- ODE.FunSpace.dist_iterate_iterate_next_le_of_lipschitzWithproof · cited by 1
- Order.succ_iterateproof · cited by 1
- ODE.FunSpace.dist_iterate_next_leproof · cited by 1
- MonoidHom.FixedPointFree.prod_pow_eq_oneproof · cited by 1
- Polynomial.deriv_gaussian_eq_hermite_mul_gaussianproof · cited by 1
- Polynomial.aeval_iterate_derivative_selfproof · cited by 1
- Polynomial.natDegree_iterate_derivativeproof · cited by 1
- Polynomial.Chebyshev.T_iterate_derivative_mem_span_Tproof · cited by 1
- Order.pred_iterateproof · cited by 0
- Polynomial.sumIDeriv_Cproof · cited by 0