Mathlib Map

Theorems · Theorem · dynamical systems

Function.iterate_one

∀ {α : Type u} (f : α → α), f^[1] = f
Defined in
Mathlib.Logic.Function.Iterate
Cited by
34 results in Mathlib
Foundations
Depth 7 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Function.minimalPeriod_eq_one_iff_isFixedPt · cited by 5Function.minimalPeriod_eq…strictMonoOn_of_lt_succ · cited by 4strictMonoOn_of_lt_succstrictMonoOn_of_pred_lt · cited by 3strictMonoOn_of_pred_ltOrdinal.omega0_lt_epsilon · cited by 2Ordinal.omega0_lt_epsilonSkewPolynomial.X_mul · cited by 2SkewPolynomial.X_mulSkewPolynomial.X_pow_eq_monomial · cited by 2SkewPolynomial.X_pow_eq_m…iter_deriv_inv_linear · cited by 2iter_deriv_inv_linearFunction.Involutive.iterate_odd · cited by 2Involutive.iterate_oddPolynomial.Chebyshev.derivative_U_eval_one · cited by 2Chebyshev.derivative_U_ev…Polynomial.iterate_derivative_derivative_mul_X · cited by 2Polynomial.iterate_deriva…Polynomial.iterate_derivative_derivative_mul_X_sq · cited by 2Polynomial.iterate_deriva…strictConcaveOn_sin_Icc · cited by 2strictConcaveOn_sin_IccOrdinal.epsilon_zero_lt_gamma · cited by 2Ordinal.epsilon_zero_lt_g…Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T · cited by 1Chebyshev.one_sub_X_sq_mu…Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U · cited by 1Chebyshev.one_sub_X_sq_mu…Nat.iterate · cited by 740Nat.iterateFunction.iterate_oneCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by34

Results whose statement or proof uses this declaration.