Theorems · Theorem · number theory
Function.Involutive.iterate_eq_id
∀ {α : Type u_4} {f : α → α} {n : ℕ}, Function.Involutive f → f ≠ id → (f^[n] = id ↔ Even n)- Defined in
- Mathlib.Algebra.Ring.Parity
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Evenstatement · cited by 444
- Oddproof · cited by 364
- Function.Involutivestatement and proof · cited by 103
- Nat.not_odd_iff_evenproof · cited by 12
- Function.Involutive.iterate_evenproof · cited by 2
- Function.Involutive.iterate_oddproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.