Theorems · Theorem · dynamical systems
Function.Injective.iterate
∀ {α : Type u} {f : α → α}, Function.Injective f → ∀ (n : ℕ), Function.Injective f^[n]- Defined in
- Mathlib.Logic.Function.Iterate
- Cited by
- 11 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 and proof · cited by 740
Cited by11
Results whose statement or proof uses this declaration.
- IsLeftRegular.powproof · cited by 5
- Module.End.HasUnifEigenvalue.ltproof · cited by 4
- IsAddLeftRegular.nsmulproof · cited by 4
- IsAddRightRegular.nsmulproof · cited by 3
- IsRightRegular.powproof · cited by 3
- FiniteField.Matrix.charpoly_pow_cardproof · cited by 2
- Function.iterate_add_eq_iterateproof · cited by 1
- MonoidHom.map_iterate_frobeniusEquiv_symmproof · cited by 1
- pNilradical_eq_bot_of_frobenius_injproof · cited by 1
- PerfectClosure.eq_iffproof · cited by 0
- Function.Bijective.iterateproof · cited by 0